Theorem difeq2 4075

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 2854	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 321	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3425	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3915	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3915	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2825	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2146  {crab 3418   ∖ cdif 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-dif 3909

This theorem is used by:  difeq12  4076  difeq2i  4078  difeq2d  4081  symdifeq1  4208  ssdifim  4226  disjdif2  4443  ssdifeq0  4449  xpdifcnvepel  6168  sorpsscmpl  7741  2oconcl  8494  oev  8505  sbthlem2  9083  sbth  9092  sbthfi  9190  infdiffi  9634  fin1ai  10292  fin23lem7  10315  fin23lem11  10316  compsscnv  10370  isf34lem1  10371  compss  10375  isf34lem4  10376  fin1a2lem7  10405  pwfseqlem4a  10661  pwfseqlem4  10662  efgmval  19826  efgi  19833  frgpuptinv  19885  gsumcllem  20022  gsumzaddlem  20035  selvfval  22320  fctop  23211  cctop  23213  iscld  23234  clsval2  23257  opncldf1  23291  opncldf2  23292  opncldf3  23293  indiscld  23298  mretopd  23299  restcld  23379  lecldbas  23426  pnrmopn  23550  hauscmplem  23613  elpt  23780  elptr  23781  cfinfil  24101  csdfil  24102  ufilss  24113  filufint  24128  cfinufil  24136  ufinffr  24137  ufilen  24138  prdsxmslem2  24737  lebnumlem1  25171  bcth3  25541  ismbl  25736  ishpg  29092  plngval  29110  frgrwopregasn  30738  frgrwopregbsn  30739  disjdifprg  32991  0elsiga  34568  prsiga  34585  sigaclci  34586  difunielsiga  34587  unelldsys  34613  sigapildsyslem  34616  sigapildsys  34617  ldgenpisyslem1  34618  isros  34623  unelros  34626  difelros  34627  inelsros  34633  diffiunisros  34634  rossros  34635  elcarsg  34760  ballotlemfval  34945  ballotlemgval  34979  kur14lem1  35735  topdifinffinlem  38050  topdifinffin  38051  oe0rif  44070  dssmapfv3d  44803  dssmapnvod  44804  clsk3nimkb  44824  ntrclsneine0lem  44848  ntrclsk2  44852  ntrclskb  44853  ntrclsk13  44855  ntrclsk4  44856  prsal  47090  saldifcl  47091  salexct  47106  salexct2  47111  salexct3  47114  salgencntex  47115  salgensscntex  47116  caragenel  47267  opncldeqv  49737