Theorem difeq2 4083

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ∈ wcel 2149  {crab 3423   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-dif 3916

This theorem is referenced by:  difeq12  4084  difeq2i  4086  difeq2d  4089  symdifeq1  4216  ssdifim  4234  disjdif2  4446  ssdifeq0  4452  xpdifcnvepel  6167  sorpsscmpl  7732  2oconcl  8487  oev  8498  sbthlem2  9075  sbth  9084  sbthfi  9182  infdiffi  9626  fin1ai  10276  fin23lem7  10299  fin23lem11  10300  compsscnv  10354  isf34lem1  10355  compss  10359  isf34lem4  10360  fin1a2lem7  10389  pwfseqlem4a  10645  pwfseqlem4  10646  efgmval  19781  efgi  19788  frgpuptinv  19840  gsumcllem  19977  gsumzaddlem  19990  selvfval  22238  fctop  23129  cctop  23131  iscld  23152  clsval2  23175  opncldf1  23209  opncldf2  23210  opncldf3  23211  indiscld  23216  mretopd  23217  restcld  23297  lecldbas  23344  pnrmopn  23468  hauscmplem  23531  elpt  23697  elptr  23698  cfinfil  24018  csdfil  24019  ufilss  24030  filufint  24045  cfinufil  24053  ufinffr  24054  ufilen  24055  prdsxmslem2  24654  lebnumlem1  25088  bcth3  25458  ismbl  25653  ishpg  28999  plngval  29016  frgrwopregasn  30607  frgrwopregbsn  30608  disjdifprg  32860  0elsiga  34448  prsiga  34465  sigaclci  34466  difelsiga  34467  unelldsys  34492  sigapildsyslem  34495  sigapildsys  34496  ldgenpisyslem1  34497  isros  34502  unelros  34505  difelros  34506  inelsros  34512  diffiunisros  34513  rossros  34514  elcarsg  34639  ballotlemfval  34824  ballotlemgval  34858  kur14lem1  35596  topdifinffinlem  37880  topdifinffin  37881  oe0rif  43903  dssmapfv3d  44636  dssmapnvod  44637  clsk3nimkb  44657  ntrclsneine0lem  44681  ntrclsk2  44685  ntrclskb  44686  ntrclsk13  44688  ntrclsk4  44689  prsal  46923  saldifcl  46924  salexct  46939  salexct2  46944  salexct3  46947  salgencntex  46948  salgensscntex  46949  caragenel  47100  opncldeqv  49564