Theorem difeq2 4056

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ∈ wcel 2144  {crab 3412   ∖ cdif 4044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 4046

This theorem is used by:  difeq12  4057  difeq2i  4059  difeq2d  4062  symdifeq1  4199  ssdifim  4217  disjdif2  4435  ssdifeq0  4441  xpdifcnvepel  6162  sorpsscmpl  7754  2oconcl  8519  oev  8530  sbthlem2  9115  sbth  9124  sbthfi  9222  infdiffi  9666  fin1ai  10378  fin23lem7  10401  fin23lem11  10402  compsscnv  10456  isf34lem1  10457  compss  10461  isf34lem4  10462  fin1a2lem7  10491  pwfseqlem4a  10753  pwfseqlem4  10754  efgmval  19935  efgi  19942  frgpuptinv  19994  gsumcllem  20131  gsumzaddlem  20144  selvfval  22437  fctop  23331  cctop  23333  iscld  23354  clsval2  23377  opncldf1  23411  opncldf2  23412  opncldf3  23413  indiscld  23418  mretopd  23419  restcld  23499  lecldbas  23546  pnrmopn  23670  hauscmplem  23733  elpt  23900  elptr  23901  cfinfil  24221  csdfil  24222  ufilss  24233  filufint  24248  cfinufil  24256  ufinffr  24257  ufilen  24258  prdsxmslem2  24857  lebnumlem1  25291  bcth3  25661  ismbl  25856  ishpg  29246  plngval  29264  frgrwopregasn  30926  frgrwopregbsn  30927  disjdifprg  33220  0elsiga  34796  prsiga  34813  sigaclci  34814  difunielsiga  34815  unelldsys  34841  sigapildsyslem  34844  sigapildsys  34845  ldgenpisyslem1  34846  isros  34851  unelros  34854  difelros  34855  inelsros  34861  diffiunisros  34862  rossros  34863  elcarsg  34987  ballotlemfval  35172  ballotlemgval  35206  kur14lem1  36089  topdifinffinlem  38407  topdifinffin  38408  oe0rif  44424  dssmapfv3d  45156  dssmapnvod  45157  clsk3nimkb  45177  ntrclsneine0lem  45201  ntrclsk2  45205  ntrclskb  45206  ntrclsk13  45208  ntrclsk4  45209  prsal  47464  saldifcl  47465  salexct  47480  salexct2  47485  salexct3  47488  salgencntex  47489  salgensscntex  47490  caragenel  47641  opncldbid  50152