Theorem difeq2 3920

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 2867	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 310	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3373	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3778	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3778	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1653   ∈ wcel 2157  {crab 3093   ∖ cdif 3766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-ral 3094  df-rab 3098  df-dif 3772

This theorem is referenced by:  difeq12  3921  difeq2i  3923  difeq2d  3926  symdifeq1  4043  ssdifim  4063  disjdif2  4241  ssdifeq0  4245  sorpsscmpl  7182  2oconcl  7823  oev  7834  sbthlem2  8313  sbth  8322  infdiffi  8805  fin1ai  9403  fin23lem7  9426  fin23lem11  9427  compsscnv  9481  isf34lem1  9482  compss  9486  isf34lem4  9487  fin1a2lem7  9516  pwfseqlem4a  9771  pwfseqlem4  9772  efgmval  18438  efgi  18445  frgpuptinv  18499  gsumcllem  18624  gsumzaddlem  18636  fctop  21137  cctop  21139  iscld  21160  clsval2  21183  opncldf1  21217  opncldf2  21218  opncldf3  21219  indiscld  21224  mretopd  21225  restcld  21305  lecldbas  21352  pnrmopn  21476  hauscmplem  21538  elpt  21704  elptr  21705  cfinfil  22025  csdfil  22026  ufilss  22037  filufint  22052  cfinufil  22060  ufinffr  22061  ufilen  22062  prdsxmslem2  22662  lebnumlem1  23088  bcth3  23457  ismbl  23634  ishpg  26007  frgrwopregasn  27665  frgrwopregbsn  27666  disjdifprg  29905  0elsiga  30693  prsiga  30710  sigaclci  30711  difelsiga  30712  unelldsys  30737  sigapildsyslem  30740  sigapildsys  30741  ldgenpisyslem1  30742  isros  30747  unelros  30750  difelros  30751  inelsros  30757  diffiunisros  30758  rossros  30759  elcarsg  30883  ballotlemfval  31068  ballotlemgval  31102  kur14lem1  31705  topdifinffinlem  33693  topdifinffin  33694  dssmapfv3d  39095  dssmapnvod  39096  clsk3nimkb  39120  ntrclsneine0lem  39144  ntrclsk2  39148  ntrclskb  39149  ntrclsk13  39151  ntrclsk4  39152  prsal  41281  saldifcl  41282  salexct  41295  salexct2  41300  salexct3  41303  salgencntex  41304  salgensscntex  41305  caragenel  41455