Theorem difeq2 4074

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 2851	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 320	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3421	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3913	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3913	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2822	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1560   ∈ wcel 2142  {crab 3414   ∖ cdif 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-dif 3907

This theorem is referenced by:  difeq12  4075  difeq2i  4077  difeq2d  4080  symdifeq1  4207  ssdifim  4225  disjdif2  4434  ssdifeq0  4440  xpdifcnvepel  6154  sorpsscmpl  7717  2oconcl  8472  oev  8483  sbthlem2  9060  sbth  9069  sbthfi  9167  infdiffi  9613  fin1ai  10250  fin23lem7  10273  fin23lem11  10274  compsscnv  10328  isf34lem1  10329  compss  10333  isf34lem4  10334  fin1a2lem7  10363  pwfseqlem4a  10619  pwfseqlem4  10620  efgmval  19752  efgi  19759  frgpuptinv  19811  gsumcllem  19948  gsumzaddlem  19961  selvfval  22172  fctop  23064  cctop  23066  iscld  23087  clsval2  23110  opncldf1  23144  opncldf2  23145  opncldf3  23146  indiscld  23151  mretopd  23152  restcld  23232  lecldbas  23279  pnrmopn  23403  hauscmplem  23466  elpt  23632  elptr  23633  cfinfil  23953  csdfil  23954  ufilss  23965  filufint  23980  cfinufil  23988  ufinffr  23989  ufilen  23990  prdsxmslem2  24589  lebnumlem1  25023  bcth3  25393  ismbl  25588  ishpg  28932  plngval  28984  frgrwopregasn  30518  frgrwopregbsn  30519  disjdifprg  32775  0elsiga  34411  prsiga  34428  sigaclci  34429  difelsiga  34430  unelldsys  34455  sigapildsyslem  34458  sigapildsys  34459  ldgenpisyslem1  34460  isros  34465  unelros  34468  difelros  34469  inelsros  34475  diffiunisros  34476  rossros  34477  elcarsg  34602  ballotlemfval  34787  ballotlemgval  34821  kur14lem1  35556  topdifinffinlem  37841  topdifinffin  37842  oe0rif  43862  dssmapfv3d  44595  dssmapnvod  44596  clsk3nimkb  44616  ntrclsneine0lem  44640  ntrclsk2  44644  ntrclskb  44645  ntrclsk13  44647  ntrclsk4  44648  prsal  46892  saldifcl  46893  salexct  46908  salexct2  46913  salexct3  46916  salgencntex  46917  salgensscntex  46918  caragenel  47069  opncldeqv  49523