Theorem difeq2 4143

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2108  {crab 3443   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-dif 3979

This theorem is referenced by:  difeq12  4144  difeq2i  4146  difeq2d  4149  symdifeq1  4274  ssdifim  4292  disjdif2  4503  ssdifeq0  4510  sorpsscmpl  7769  2oconcl  8559  oev  8570  sbthlem2  9150  sbth  9159  sbthfi  9265  infdiffi  9727  fin1ai  10362  fin23lem7  10385  fin23lem11  10386  compsscnv  10440  isf34lem1  10441  compss  10445  isf34lem4  10446  fin1a2lem7  10475  pwfseqlem4a  10730  pwfseqlem4  10731  efgmval  19754  efgi  19761  frgpuptinv  19813  gsumcllem  19950  gsumzaddlem  19963  selvfval  22161  fctop  23032  cctop  23034  iscld  23056  clsval2  23079  opncldf1  23113  opncldf2  23114  opncldf3  23115  indiscld  23120  mretopd  23121  restcld  23201  lecldbas  23248  pnrmopn  23372  hauscmplem  23435  elpt  23601  elptr  23602  cfinfil  23922  csdfil  23923  ufilss  23934  filufint  23949  cfinufil  23957  ufinffr  23958  ufilen  23959  prdsxmslem2  24563  lebnumlem1  25012  bcth3  25384  ismbl  25580  ishpg  28785  frgrwopregasn  30348  frgrwopregbsn  30349  disjdifprg  32597  0elsiga  34078  prsiga  34095  sigaclci  34096  difelsiga  34097  unelldsys  34122  sigapildsyslem  34125  sigapildsys  34126  ldgenpisyslem1  34127  isros  34132  unelros  34135  difelros  34136  inelsros  34142  diffiunisros  34143  rossros  34144  elcarsg  34270  ballotlemfval  34454  ballotlemgval  34488  kur14lem1  35174  topdifinffinlem  37313  topdifinffin  37314  oe0rif  43247  dssmapfv3d  43981  dssmapnvod  43982  clsk3nimkb  44002  ntrclsneine0lem  44026  ntrclsk2  44030  ntrclskb  44031  ntrclsk13  44033  ntrclsk4  44034  prsal  46239  saldifcl  46240  salexct  46255  salexct2  46260  salexct3  46263  salgencntex  46264  salgensscntex  46265  caragenel  46416  opncldeqv  48581