Theorem difeq2 4052

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2107  {crab 3069   ∖ cdif 3885

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-dif 3891

This theorem is referenced by:  difeq12  4053  difeq2i  4055  difeq2d  4058  symdifeq1  4179  ssdifim  4197  disjdif2  4414  ssdifeq0  4418  sorpsscmpl  7596  2oconcl  8342  oev  8353  sbthlem2  8880  sbth  8889  sbthfi  8994  infdiffi  9425  fin1ai  10058  fin23lem7  10081  fin23lem11  10082  compsscnv  10136  isf34lem1  10137  compss  10141  isf34lem4  10142  fin1a2lem7  10171  pwfseqlem4a  10426  pwfseqlem4  10427  efgmval  19327  efgi  19334  frgpuptinv  19386  gsumcllem  19518  gsumzaddlem  19531  selvfval  21336  fctop  22163  cctop  22165  iscld  22187  clsval2  22210  opncldf1  22244  opncldf2  22245  opncldf3  22246  indiscld  22251  mretopd  22252  restcld  22332  lecldbas  22379  pnrmopn  22503  hauscmplem  22566  elpt  22732  elptr  22733  cfinfil  23053  csdfil  23054  ufilss  23065  filufint  23080  cfinufil  23088  ufinffr  23089  ufilen  23090  prdsxmslem2  23694  lebnumlem1  24133  bcth3  24504  ismbl  24699  ishpg  27129  frgrwopregasn  28689  frgrwopregbsn  28690  disjdifprg  30923  0elsiga  32091  prsiga  32108  sigaclci  32109  difelsiga  32110  unelldsys  32135  sigapildsyslem  32138  sigapildsys  32139  ldgenpisyslem1  32140  isros  32145  unelros  32148  difelros  32149  inelsros  32155  diffiunisros  32156  rossros  32157  elcarsg  32281  ballotlemfval  32465  ballotlemgval  32499  kur14lem1  33177  topdifinffinlem  35527  topdifinffin  35528  dssmapfv3d  41634  dssmapnvod  41635  clsk3nimkb  41657  ntrclsneine0lem  41681  ntrclsk2  41685  ntrclskb  41686  ntrclsk13  41688  ntrclsk4  41689  prsal  43866  saldifcl  43867  salexct  43880  salexct2  43885  salexct3  43888  salgencntex  43889  salgensscntex  43890  caragenel  44040  opncldeqv  46206