Theorem difeq2 4047

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2108  {crab 3067   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-dif 3886

This theorem is referenced by:  difeq12  4048  difeq2i  4050  difeq2d  4053  symdifeq1  4175  ssdifim  4193  disjdif2  4410  ssdifeq0  4414  sorpsscmpl  7565  2oconcl  8295  oev  8306  sbthlem2  8824  sbth  8833  sbthfi  8942  infdiffi  9346  fin1ai  9980  fin23lem7  10003  fin23lem11  10004  compsscnv  10058  isf34lem1  10059  compss  10063  isf34lem4  10064  fin1a2lem7  10093  pwfseqlem4a  10348  pwfseqlem4  10349  efgmval  19233  efgi  19240  frgpuptinv  19292  gsumcllem  19424  gsumzaddlem  19437  selvfval  21237  fctop  22062  cctop  22064  iscld  22086  clsval2  22109  opncldf1  22143  opncldf2  22144  opncldf3  22145  indiscld  22150  mretopd  22151  restcld  22231  lecldbas  22278  pnrmopn  22402  hauscmplem  22465  elpt  22631  elptr  22632  cfinfil  22952  csdfil  22953  ufilss  22964  filufint  22979  cfinufil  22987  ufinffr  22988  ufilen  22989  prdsxmslem2  23591  lebnumlem1  24030  bcth3  24400  ismbl  24595  ishpg  27024  frgrwopregasn  28581  frgrwopregbsn  28582  disjdifprg  30815  0elsiga  31982  prsiga  31999  sigaclci  32000  difelsiga  32001  unelldsys  32026  sigapildsyslem  32029  sigapildsys  32030  ldgenpisyslem1  32031  isros  32036  unelros  32039  difelros  32040  inelsros  32046  diffiunisros  32047  rossros  32048  elcarsg  32172  ballotlemfval  32356  ballotlemgval  32390  kur14lem1  33068  topdifinffinlem  35445  topdifinffin  35446  dssmapfv3d  41516  dssmapnvod  41517  clsk3nimkb  41539  ntrclsneine0lem  41563  ntrclsk2  41567  ntrclskb  41568  ntrclsk13  41570  ntrclsk4  41571  prsal  43749  saldifcl  43750  salexct  43763  salexct2  43768  salexct3  43771  salgencntex  43772  salgensscntex  43773  caragenel  43923  opncldeqv  46083