Theorem difeq2 4079

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 3410	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3920	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3920	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

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

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 3403  df-dif 3914

This theorem is referenced by:  difeq12  4080  difeq2i  4082  difeq2d  4085  symdifeq1  4214  ssdifim  4232  disjdif2  4439  ssdifeq0  4446  sorpsscmpl  7690  2oconcl  8444  oev  8455  sbthlem2  9029  sbth  9038  sbthfi  9140  infdiffi  9587  fin1ai  10222  fin23lem7  10245  fin23lem11  10246  compsscnv  10300  isf34lem1  10301  compss  10305  isf34lem4  10306  fin1a2lem7  10335  pwfseqlem4a  10590  pwfseqlem4  10591  efgmval  19626  efgi  19633  frgpuptinv  19685  gsumcllem  19822  gsumzaddlem  19835  selvfval  22054  fctop  22924  cctop  22926  iscld  22947  clsval2  22970  opncldf1  23004  opncldf2  23005  opncldf3  23006  indiscld  23011  mretopd  23012  restcld  23092  lecldbas  23139  pnrmopn  23263  hauscmplem  23326  elpt  23492  elptr  23493  cfinfil  23813  csdfil  23814  ufilss  23825  filufint  23840  cfinufil  23848  ufinffr  23849  ufilen  23850  prdsxmslem2  24450  lebnumlem1  24893  bcth3  25264  ismbl  25460  ishpg  28739  frgrwopregasn  30295  frgrwopregbsn  30296  disjdifprg  32554  0elsiga  34097  prsiga  34114  sigaclci  34115  difelsiga  34116  unelldsys  34141  sigapildsyslem  34144  sigapildsys  34145  ldgenpisyslem1  34146  isros  34151  unelros  34154  difelros  34155  inelsros  34161  diffiunisros  34162  rossros  34163  elcarsg  34289  ballotlemfval  34474  ballotlemgval  34508  kur14lem1  35186  topdifinffinlem  37328  topdifinffin  37329  oe0rif  43267  dssmapfv3d  44001  dssmapnvod  44002  clsk3nimkb  44022  ntrclsneine0lem  44046  ntrclsk2  44050  ntrclskb  44051  ntrclsk13  44053  ntrclsk4  44054  prsal  46309  saldifcl  46310  salexct  46325  salexct2  46330  salexct3  46333  salgencntex  46334  salgensscntex  46335  caragenel  46486  opncldeqv  48883