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

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

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 3395  df-dif 3906

This theorem is referenced by:  difeq12  4072  difeq2i  4074  difeq2d  4077  symdifeq1  4206  ssdifim  4224  disjdif2  4431  ssdifeq0  4438  sorpsscmpl  7670  2oconcl  8421  oev  8432  sbthlem2  9005  sbth  9014  sbthfi  9113  infdiffi  9554  fin1ai  10187  fin23lem7  10210  fin23lem11  10211  compsscnv  10265  isf34lem1  10266  compss  10270  isf34lem4  10271  fin1a2lem7  10300  pwfseqlem4a  10555  pwfseqlem4  10556  efgmval  19591  efgi  19598  frgpuptinv  19650  gsumcllem  19787  gsumzaddlem  19800  selvfval  22019  fctop  22889  cctop  22891  iscld  22912  clsval2  22935  opncldf1  22969  opncldf2  22970  opncldf3  22971  indiscld  22976  mretopd  22977  restcld  23057  lecldbas  23104  pnrmopn  23228  hauscmplem  23291  elpt  23457  elptr  23458  cfinfil  23778  csdfil  23779  ufilss  23790  filufint  23805  cfinufil  23813  ufinffr  23814  ufilen  23815  prdsxmslem2  24415  lebnumlem1  24858  bcth3  25229  ismbl  25425  ishpg  28704  frgrwopregasn  30260  frgrwopregbsn  30261  disjdifprg  32519  0elsiga  34081  prsiga  34098  sigaclci  34099  difelsiga  34100  unelldsys  34125  sigapildsyslem  34128  sigapildsys  34129  ldgenpisyslem1  34130  isros  34135  unelros  34138  difelros  34139  inelsros  34145  diffiunisros  34146  rossros  34147  elcarsg  34273  ballotlemfval  34458  ballotlemgval  34492  kur14lem1  35179  topdifinffinlem  37321  topdifinffin  37322  oe0rif  43258  dssmapfv3d  43992  dssmapnvod  43993  clsk3nimkb  44013  ntrclsneine0lem  44037  ntrclsk2  44041  ntrclskb  44042  ntrclsk13  44044  ntrclsk4  44045  prsal  46299  saldifcl  46300  salexct  46315  salexct2  46320  salexct3  46323  salgencntex  46324  salgensscntex  46325  caragenel  46476  opncldeqv  48886