Theorem difeq2 3714

Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
difeq2	⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Proof of Theorem difeq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2688	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 308	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3184	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3576	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3576	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2679	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1481   ∈ wcel 1988  {crab 2913   ∖ cdif 3564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-ral 2914  df-rab 2918  df-dif 3570

This theorem is referenced by:  difeq12  3715  difeq2i  3717  difeq2d  3720  symdifeq1  3838  ssdifim  3854  disjdif2  4038  ssdifeq0  4042  sorpsscmpl  6933  2oconcl  7568  oev  7579  sbthlem2  8056  sbth  8065  infdiffi  8540  fin1ai  9100  fin23lem7  9123  fin23lem11  9124  compsscnv  9178  isf34lem1  9179  compss  9183  isf34lem4  9184  fin1a2lem7  9213  pwfseqlem4a  9468  pwfseqlem4  9469  efgmval  18106  efgi  18113  frgpuptinv  18165  gsumcllem  18290  gsumzaddlem  18302  fctop  20789  cctop  20791  iscld  20812  clsval2  20835  opncldf1  20869  opncldf2  20870  opncldf3  20871  indiscld  20876  mretopd  20877  restcld  20957  lecldbas  21004  pnrmopn  21128  hauscmplem  21190  elpt  21356  elptr  21357  cfinfil  21678  csdfil  21679  ufilss  21690  filufint  21705  cfinufil  21713  ufinffr  21714  ufilen  21715  prdsxmslem2  22315  lebnumlem1  22741  bcth3  23109  ismbl  23275  ishpg  25632  frgrwopreg1  27160  frgrwopreg2  27161  disjdifprg  29360  0elsiga  30151  prsiga  30168  sigaclci  30169  difelsiga  30170  unelldsys  30195  sigapildsyslem  30198  sigapildsys  30199  ldgenpisyslem1  30200  isros  30205  unelros  30208  difelros  30209  inelsros  30215  diffiunisros  30216  rossros  30217  elcarsg  30341  ballotlemfval  30525  ballotlemgval  30559  kur14lem1  31162  topdifinffinlem  33166  topdifinffin  33167  dssmapfv3d  38133  dssmapnvod  38134  clsk3nimkb  38158  ntrclsneine0lem  38182  ntrclsk2  38186  ntrclskb  38187  ntrclsk13  38189  ntrclsk4  38190  prsal  40301  saldifcl  40302  salexct  40315  salexct2  40320  salexct3  40323  salgencntex  40324  salgensscntex  40325  caragenel  40472