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

Theorem difeq2 3755
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 2719 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21notbid 307 . . 3 (𝐴 = 𝐵 → (¬ 𝑥𝐴 ↔ ¬ 𝑥𝐵))
32rabbidv 3220 . 2 (𝐴 = 𝐵 → {𝑥𝐶 ∣ ¬ 𝑥𝐴} = {𝑥𝐶 ∣ ¬ 𝑥𝐵})
4 dfdif2 3616 . 2 (𝐶𝐴) = {𝑥𝐶 ∣ ¬ 𝑥𝐴}
5 dfdif2 3616 . 2 (𝐶𝐵) = {𝑥𝐶 ∣ ¬ 𝑥𝐵}
63, 4, 53eqtr4g 2710 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wcel 2030  {crab 2945  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-rab 2950  df-dif 3610
This theorem is referenced by:  difeq12  3756  difeq2i  3758  difeq2d  3761  symdifeq1  3879  ssdifim  3895  disjdif2  4080  ssdifeq0  4084  sorpsscmpl  6990  2oconcl  7628  oev  7639  sbthlem2  8112  sbth  8121  infdiffi  8593  fin1ai  9153  fin23lem7  9176  fin23lem11  9177  compsscnv  9231  isf34lem1  9232  compss  9236  isf34lem4  9237  fin1a2lem7  9266  pwfseqlem4a  9521  pwfseqlem4  9522  efgmval  18171  efgi  18178  frgpuptinv  18230  gsumcllem  18355  gsumzaddlem  18367  fctop  20856  cctop  20858  iscld  20879  clsval2  20902  opncldf1  20936  opncldf2  20937  opncldf3  20938  indiscld  20943  mretopd  20944  restcld  21024  lecldbas  21071  pnrmopn  21195  hauscmplem  21257  elpt  21423  elptr  21424  cfinfil  21744  csdfil  21745  ufilss  21756  filufint  21771  cfinufil  21779  ufinffr  21780  ufilen  21781  prdsxmslem2  22381  lebnumlem1  22807  bcth3  23174  ismbl  23340  ishpg  25696  frgrwopregasn  27296  frgrwopregbsn  27297  disjdifprg  29514  0elsiga  30305  prsiga  30322  sigaclci  30323  difelsiga  30324  unelldsys  30349  sigapildsyslem  30352  sigapildsys  30353  ldgenpisyslem1  30354  isros  30359  unelros  30362  difelros  30363  inelsros  30369  diffiunisros  30370  rossros  30371  elcarsg  30495  ballotlemfval  30679  ballotlemgval  30713  kur14lem1  31314  topdifinffinlem  33325  topdifinffin  33326  dssmapfv3d  38630  dssmapnvod  38631  clsk3nimkb  38655  ntrclsneine0lem  38679  ntrclsk2  38683  ntrclskb  38684  ntrclsk13  38686  ntrclsk4  38687  prsal  40856  saldifcl  40857  salexct  40870  salexct2  40875  salexct3  40878  salgencntex  40879  salgensscntex  40880  caragenel  41030
  Copyright terms: Public domain W3C validator