Theorem difeq2 4051

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 2828	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 319	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3398	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3892	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3892	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ∈ wcel 2119  {crab 3391   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-dif 3886

This theorem is referenced by:  difeq12  4052  difeq2i  4054  difeq2d  4057  symdifeq1  4183  ssdifim  4201  disjdif2  4408  ssdifeq0  4414  sorpsscmpl  7677  2oconcl  8428  oev  8439  sbthlem2  9016  sbth  9025  sbthfi  9123  infdiffi  9570  fin1ai  10206  fin23lem7  10229  fin23lem11  10230  compsscnv  10284  isf34lem1  10285  compss  10289  isf34lem4  10290  fin1a2lem7  10319  pwfseqlem4a  10575  pwfseqlem4  10576  efgmval  19678  efgi  19685  frgpuptinv  19737  gsumcllem  19874  gsumzaddlem  19887  selvfval  22095  fctop  22987  cctop  22989  iscld  23010  clsval2  23033  opncldf1  23067  opncldf2  23068  opncldf3  23069  indiscld  23074  mretopd  23075  restcld  23155  lecldbas  23202  pnrmopn  23326  hauscmplem  23389  elpt  23555  elptr  23556  cfinfil  23876  csdfil  23877  ufilss  23888  filufint  23903  cfinufil  23911  ufinffr  23912  ufilen  23913  prdsxmslem2  24512  lebnumlem1  24946  bcth3  25316  ismbl  25511  ishpg  28845  frgrwopregasn  30404  frgrwopregbsn  30405  disjdifprg  32664  0elsiga  34298  prsiga  34315  sigaclci  34316  difelsiga  34317  unelldsys  34342  sigapildsyslem  34345  sigapildsys  34346  ldgenpisyslem1  34347  isros  34352  unelros  34355  difelros  34356  inelsros  34362  diffiunisros  34363  rossros  34364  elcarsg  34489  ballotlemfval  34674  ballotlemgval  34708  kur14lem1  35434  topdifinffinlem  37709  topdifinffin  37710  oe0rif  43730  dssmapfv3d  44463  dssmapnvod  44464  clsk3nimkb  44484  ntrclsneine0lem  44508  ntrclsk2  44512  ntrclskb  44513  ntrclsk13  44515  ntrclsk4  44516  prsal  46761  saldifcl  46762  salexct  46777  salexct2  46782  salexct3  46785  salgencntex  46786  salgensscntex  46787  caragenel  46938  opncldeqv  49392