Theorem difeq2 4070

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-dif 3902

This theorem is referenced by:  difeq12  4071  difeq2i  4073  difeq2d  4076  symdifeq1  4205  ssdifim  4223  disjdif2  4430  ssdifeq0  4437  sorpsscmpl  7677  2oconcl  8428  oev  8439  sbthlem2  9014  sbth  9023  sbthfi  9121  infdiffi  9565  fin1ai  10201  fin23lem7  10224  fin23lem11  10225  compsscnv  10279  isf34lem1  10280  compss  10284  isf34lem4  10285  fin1a2lem7  10314  pwfseqlem4a  10570  pwfseqlem4  10571  efgmval  19639  efgi  19646  frgpuptinv  19698  gsumcllem  19835  gsumzaddlem  19848  selvfval  22075  fctop  22946  cctop  22948  iscld  22969  clsval2  22992  opncldf1  23026  opncldf2  23027  opncldf3  23028  indiscld  23033  mretopd  23034  restcld  23114  lecldbas  23161  pnrmopn  23285  hauscmplem  23348  elpt  23514  elptr  23515  cfinfil  23835  csdfil  23836  ufilss  23847  filufint  23862  cfinufil  23870  ufinffr  23871  ufilen  23872  prdsxmslem2  24471  lebnumlem1  24914  bcth3  25285  ismbl  25481  ishpg  28780  frgrwopregasn  30340  frgrwopregbsn  30341  disjdifprg  32599  0elsiga  34220  prsiga  34237  sigaclci  34238  difelsiga  34239  unelldsys  34264  sigapildsyslem  34267  sigapildsys  34268  ldgenpisyslem1  34269  isros  34274  unelros  34277  difelros  34278  inelsros  34284  diffiunisros  34285  rossros  34286  elcarsg  34411  ballotlemfval  34596  ballotlemgval  34630  kur14lem1  35349  topdifinffinlem  37491  topdifinffin  37492  oe0rif  43469  dssmapfv3d  44202  dssmapnvod  44203  clsk3nimkb  44223  ntrclsneine0lem  44247  ntrclsk2  44251  ntrclskb  44252  ntrclsk13  44254  ntrclsk4  44255  prsal  46504  saldifcl  46505  salexct  46520  salexct2  46525  salexct3  46528  salgencntex  46529  salgensscntex  46530  caragenel  46681  opncldeqv  49089