Theorem difeq2 4079

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 3410	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3920	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3920	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

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

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 3403  df-dif 3914

This theorem is referenced by:  difeq12  4080  difeq2i  4082  difeq2d  4085  symdifeq1  4214  ssdifim  4232  disjdif2  4439  ssdifeq0  4446  sorpsscmpl  7690  2oconcl  8444  oev  8455  sbthlem2  9029  sbth  9038  sbthfi  9140  infdiffi  9587  fin1ai  10222  fin23lem7  10245  fin23lem11  10246  compsscnv  10300  isf34lem1  10301  compss  10305  isf34lem4  10306  fin1a2lem7  10335  pwfseqlem4a  10590  pwfseqlem4  10591  efgmval  19618  efgi  19625  frgpuptinv  19677  gsumcllem  19814  gsumzaddlem  19827  selvfval  21997  fctop  22867  cctop  22869  iscld  22890  clsval2  22913  opncldf1  22947  opncldf2  22948  opncldf3  22949  indiscld  22954  mretopd  22955  restcld  23035  lecldbas  23082  pnrmopn  23206  hauscmplem  23269  elpt  23435  elptr  23436  cfinfil  23756  csdfil  23757  ufilss  23768  filufint  23783  cfinufil  23791  ufinffr  23792  ufilen  23793  prdsxmslem2  24393  lebnumlem1  24836  bcth3  25207  ismbl  25403  ishpg  28662  frgrwopregasn  30218  frgrwopregbsn  30219  disjdifprg  32477  0elsiga  34077  prsiga  34094  sigaclci  34095  difelsiga  34096  unelldsys  34121  sigapildsyslem  34124  sigapildsys  34125  ldgenpisyslem1  34126  isros  34131  unelros  34134  difelros  34135  inelsros  34141  diffiunisros  34142  rossros  34143  elcarsg  34269  ballotlemfval  34454  ballotlemgval  34488  kur14lem1  35166  topdifinffinlem  37308  topdifinffin  37309  oe0rif  43247  dssmapfv3d  43981  dssmapnvod  43982  clsk3nimkb  44002  ntrclsneine0lem  44026  ntrclsk2  44030  ntrclskb  44031  ntrclsk13  44033  ntrclsk4  44034  prsal  46289  saldifcl  46290  salexct  46305  salexct2  46310  salexct3  46313  salgencntex  46314  salgensscntex  46315  caragenel  46466  opncldeqv  48863