Theorem difeq2 4083

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 2817	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 318	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3413	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3923	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3923	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  {crab 3405   ∖ cdif 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-dif 3917

This theorem is referenced by:  difeq12  4084  difeq2i  4086  difeq2d  4089  symdifeq1  4218  ssdifim  4236  disjdif2  4443  ssdifeq0  4450  sorpsscmpl  7710  2oconcl  8467  oev  8478  sbthlem2  9052  sbth  9061  sbthfi  9163  infdiffi  9611  fin1ai  10246  fin23lem7  10269  fin23lem11  10270  compsscnv  10324  isf34lem1  10325  compss  10329  isf34lem4  10330  fin1a2lem7  10359  pwfseqlem4a  10614  pwfseqlem4  10615  efgmval  19642  efgi  19649  frgpuptinv  19701  gsumcllem  19838  gsumzaddlem  19851  selvfval  22021  fctop  22891  cctop  22893  iscld  22914  clsval2  22937  opncldf1  22971  opncldf2  22972  opncldf3  22973  indiscld  22978  mretopd  22979  restcld  23059  lecldbas  23106  pnrmopn  23230  hauscmplem  23293  elpt  23459  elptr  23460  cfinfil  23780  csdfil  23781  ufilss  23792  filufint  23807  cfinufil  23815  ufinffr  23816  ufilen  23817  prdsxmslem2  24417  lebnumlem1  24860  bcth3  25231  ismbl  25427  ishpg  28686  frgrwopregasn  30245  frgrwopregbsn  30246  disjdifprg  32504  0elsiga  34104  prsiga  34121  sigaclci  34122  difelsiga  34123  unelldsys  34148  sigapildsyslem  34151  sigapildsys  34152  ldgenpisyslem1  34153  isros  34158  unelros  34161  difelros  34162  inelsros  34168  diffiunisros  34169  rossros  34170  elcarsg  34296  ballotlemfval  34481  ballotlemgval  34515  kur14lem1  35193  topdifinffinlem  37335  topdifinffin  37336  oe0rif  43274  dssmapfv3d  44008  dssmapnvod  44009  clsk3nimkb  44029  ntrclsneine0lem  44053  ntrclsk2  44057  ntrclskb  44058  ntrclsk13  44060  ntrclsk4  44061  prsal  46316  saldifcl  46317  salexct  46332  salexct2  46337  salexct3  46340  salgencntex  46341  salgensscntex  46342  caragenel  46493  opncldeqv  48890