Theorem difeq2 4023

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 2841	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 322	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3393	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3868	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3868	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2819	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2112  {crab 3075   ∖ cdif 3856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-rab 3080  df-dif 3862

This theorem is referenced by:  difeq12  4024  difeq2i  4026  difeq2d  4029  symdifeq1  4150  ssdifim  4168  disjdif2  4377  ssdifeq0  4381  sorpsscmpl  7459  2oconcl  8139  oev  8150  sbthlem2  8650  sbth  8659  infdiffi  9147  fin1ai  9746  fin23lem7  9769  fin23lem11  9770  compsscnv  9824  isf34lem1  9825  compss  9829  isf34lem4  9830  fin1a2lem7  9859  pwfseqlem4a  10114  pwfseqlem4  10115  efgmval  18898  efgi  18905  frgpuptinv  18957  gsumcllem  19089  gsumzaddlem  19102  selvfval  20873  fctop  21697  cctop  21699  iscld  21720  clsval2  21743  opncldf1  21777  opncldf2  21778  opncldf3  21779  indiscld  21784  mretopd  21785  restcld  21865  lecldbas  21912  pnrmopn  22036  hauscmplem  22099  elpt  22265  elptr  22266  cfinfil  22586  csdfil  22587  ufilss  22598  filufint  22613  cfinufil  22621  ufinffr  22622  ufilen  22623  prdsxmslem2  23224  lebnumlem1  23655  bcth3  24024  ismbl  24219  ishpg  26645  frgrwopregasn  28193  frgrwopregbsn  28194  disjdifprg  30429  0elsiga  31594  prsiga  31611  sigaclci  31612  difelsiga  31613  unelldsys  31638  sigapildsyslem  31641  sigapildsys  31642  ldgenpisyslem1  31643  isros  31648  unelros  31651  difelros  31652  inelsros  31658  diffiunisros  31659  rossros  31660  elcarsg  31784  ballotlemfval  31968  ballotlemgval  32002  kur14lem1  32677  topdifinffinlem  35037  topdifinffin  35038  dssmapfv3d  41086  dssmapnvod  41087  clsk3nimkb  41109  ntrclsneine0lem  41133  ntrclsk2  41137  ntrclskb  41138  ntrclsk13  41140  ntrclsk4  41141  prsal  43319  saldifcl  43320  salexct  43333  salexct2  43338  salexct3  43341  salgencntex  43342  salgensscntex  43343  caragenel  43493  opncldeqv  45571