Theorem difeq2 4068

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3413   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3902

This theorem is used by:  difeq12  4069  difeq2i  4071  difeq2d  4074  symdifeq1  4201  ssdifim  4219  disjdif2  4436  ssdifeq0  4442  xpdifcnvepel  6160  sorpsscmpl  7750  2oconcl  8511  oev  8522  sbthlem2  9107  sbth  9116  sbthfi  9214  infdiffi  9659  fin1ai  10371  fin23lem7  10394  fin23lem11  10395  compsscnv  10449  isf34lem1  10450  compss  10454  isf34lem4  10455  fin1a2lem7  10484  pwfseqlem4a  10746  pwfseqlem4  10747  efgmval  19926  efgi  19933  frgpuptinv  19985  gsumcllem  20122  gsumzaddlem  20135  selvfval  22428  fctop  23322  cctop  23324  iscld  23345  clsval2  23368  opncldf1  23402  opncldf2  23403  opncldf3  23404  indiscld  23409  mretopd  23410  restcld  23490  lecldbas  23537  pnrmopn  23661  hauscmplem  23724  elpt  23891  elptr  23892  cfinfil  24212  csdfil  24213  ufilss  24224  filufint  24239  cfinufil  24247  ufinffr  24248  ufilen  24249  prdsxmslem2  24848  lebnumlem1  25282  bcth3  25652  ismbl  25847  ishpg  29237  plngval  29255  frgrwopregasn  30917  frgrwopregbsn  30918  disjdifprg  33169  0elsiga  34746  prsiga  34763  sigaclci  34764  difunielsiga  34765  unelldsys  34791  sigapildsyslem  34794  sigapildsys  34795  ldgenpisyslem1  34796  isros  34801  unelros  34804  difelros  34805  inelsros  34811  diffiunisros  34812  rossros  34813  elcarsg  34937  ballotlemfval  35122  ballotlemgval  35156  kur14lem1  35971  topdifinffinlem  38270  topdifinffin  38271  oe0rif  44286  dssmapfv3d  45018  dssmapnvod  45019  clsk3nimkb  45039  ntrclsneine0lem  45063  ntrclsk2  45067  ntrclskb  45068  ntrclsk13  45070  ntrclsk4  45071  prsal  47327  saldifcl  47328  salexct  47343  salexct2  47348  salexct3  47351  salgencntex  47352  salgensscntex  47353  caragenel  47504  opncldbid  50009