MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difeq2 Structured version   Visualization version   GIF version

Theorem difeq2 4097
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.
StepHypRef Expression
1 eleq2 2906 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21notbid 319 . . 3 (𝐴 = 𝐵 → (¬ 𝑥𝐴 ↔ ¬ 𝑥𝐵))
32rabbidv 3486 . 2 (𝐴 = 𝐵 → {𝑥𝐶 ∣ ¬ 𝑥𝐴} = {𝑥𝐶 ∣ ¬ 𝑥𝐵})
4 dfdif2 3949 . 2 (𝐶𝐴) = {𝑥𝐶 ∣ ¬ 𝑥𝐴}
5 dfdif2 3949 . 2 (𝐶𝐵) = {𝑥𝐶 ∣ ¬ 𝑥𝐵}
63, 4, 53eqtr4g 2886 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1530  wcel 2107  {crab 3147  cdif 3937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-rab 3152  df-dif 3943
This theorem is referenced by:  difeq12  4098  difeq2i  4100  difeq2d  4103  symdifeq1  4225  ssdifim  4243  disjdif2  4431  ssdifeq0  4435  sorpsscmpl  7454  2oconcl  8124  oev  8135  sbthlem2  8622  sbth  8631  infdiffi  9115  fin1ai  9709  fin23lem7  9732  fin23lem11  9733  compsscnv  9787  isf34lem1  9788  compss  9792  isf34lem4  9793  fin1a2lem7  9822  pwfseqlem4a  10077  pwfseqlem4  10078  efgmval  18774  efgi  18781  frgpuptinv  18833  gsumcllem  18964  gsumzaddlem  18977  selvfval  20265  fctop  21547  cctop  21549  iscld  21570  clsval2  21593  opncldf1  21627  opncldf2  21628  opncldf3  21629  indiscld  21634  mretopd  21635  restcld  21715  lecldbas  21762  pnrmopn  21886  hauscmplem  21949  elpt  22115  elptr  22116  cfinfil  22436  csdfil  22437  ufilss  22448  filufint  22463  cfinufil  22471  ufinffr  22472  ufilen  22473  prdsxmslem2  23073  lebnumlem1  23499  bcth3  23868  ismbl  24061  ishpg  26478  frgrwopregasn  28028  frgrwopregbsn  28029  disjdifprg  30259  0elsiga  31278  prsiga  31295  sigaclci  31296  difelsiga  31297  unelldsys  31322  sigapildsyslem  31325  sigapildsys  31326  ldgenpisyslem1  31327  isros  31332  unelros  31335  difelros  31336  inelsros  31342  diffiunisros  31343  rossros  31344  elcarsg  31468  ballotlemfval  31652  ballotlemgval  31686  kur14lem1  32356  topdifinffinlem  34516  topdifinffin  34517  dssmapfv3d  40249  dssmapnvod  40250  clsk3nimkb  40274  ntrclsneine0lem  40298  ntrclsk2  40302  ntrclskb  40303  ntrclsk13  40305  ntrclsk4  40306  prsal  42488  saldifcl  42489  salexct  42502  salexct2  42507  salexct3  42510  salgencntex  42511  salgensscntex  42512  caragenel  42662
  Copyright terms: Public domain W3C validator