Theorem difeq2 4071

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113  {crab 3397   ∖ cdif 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-dif 3902

This theorem is referenced by:  difeq12  4072  difeq2i  4074  difeq2d  4077  symdifeq1  4206  ssdifim  4224  disjdif2  4431  ssdifeq0  4438  sorpsscmpl  7676  2oconcl  8427  oev  8438  sbthlem2  9011  sbth  9020  sbthfi  9118  infdiffi  9558  fin1ai  10194  fin23lem7  10217  fin23lem11  10218  compsscnv  10272  isf34lem1  10273  compss  10277  isf34lem4  10278  fin1a2lem7  10307  pwfseqlem4a  10562  pwfseqlem4  10563  efgmval  19634  efgi  19641  frgpuptinv  19693  gsumcllem  19830  gsumzaddlem  19843  selvfval  22059  fctop  22929  cctop  22931  iscld  22952  clsval2  22975  opncldf1  23009  opncldf2  23010  opncldf3  23011  indiscld  23016  mretopd  23017  restcld  23097  lecldbas  23144  pnrmopn  23268  hauscmplem  23331  elpt  23497  elptr  23498  cfinfil  23818  csdfil  23819  ufilss  23830  filufint  23845  cfinufil  23853  ufinffr  23854  ufilen  23855  prdsxmslem2  24454  lebnumlem1  24897  bcth3  25268  ismbl  25464  ishpg  28747  frgrwopregasn  30307  frgrwopregbsn  30308  disjdifprg  32566  0elsiga  34138  prsiga  34155  sigaclci  34156  difelsiga  34157  unelldsys  34182  sigapildsyslem  34185  sigapildsys  34186  ldgenpisyslem1  34187  isros  34192  unelros  34195  difelros  34196  inelsros  34202  diffiunisros  34203  rossros  34204  elcarsg  34329  ballotlemfval  34514  ballotlemgval  34548  kur14lem1  35261  topdifinffinlem  37402  topdifinffin  37403  oe0rif  43392  dssmapfv3d  44126  dssmapnvod  44127  clsk3nimkb  44147  ntrclsneine0lem  44171  ntrclsk2  44175  ntrclskb  44176  ntrclsk13  44178  ntrclsk4  44179  prsal  46430  saldifcl  46431  salexct  46446  salexct2  46451  salexct3  46454  salgencntex  46455  salgensscntex  46456  caragenel  46607  opncldeqv  49016