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

Theorem difeq2 4090
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 2898 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21notbid 319 . . 3 (𝐴 = 𝐵 → (¬ 𝑥𝐴 ↔ ¬ 𝑥𝐵))
32rabbidv 3478 . 2 (𝐴 = 𝐵 → {𝑥𝐶 ∣ ¬ 𝑥𝐴} = {𝑥𝐶 ∣ ¬ 𝑥𝐵})
4 dfdif2 3942 . 2 (𝐶𝐴) = {𝑥𝐶 ∣ ¬ 𝑥𝐴}
5 dfdif2 3942 . 2 (𝐶𝐵) = {𝑥𝐶 ∣ ¬ 𝑥𝐵}
63, 4, 53eqtr4g 2878 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wcel 2105  {crab 3139  cdif 3930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rab 3144  df-dif 3936
This theorem is referenced by:  difeq12  4091  difeq2i  4093  difeq2d  4096  symdifeq1  4218  ssdifim  4236  disjdif2  4424  ssdifeq0  4428  sorpsscmpl  7449  2oconcl  8117  oev  8128  sbthlem2  8616  sbth  8625  infdiffi  9109  fin1ai  9703  fin23lem7  9726  fin23lem11  9727  compsscnv  9781  isf34lem1  9782  compss  9786  isf34lem4  9787  fin1a2lem7  9816  pwfseqlem4a  10071  pwfseqlem4  10072  efgmval  18767  efgi  18774  frgpuptinv  18826  gsumcllem  18957  gsumzaddlem  18970  selvfval  20258  fctop  21540  cctop  21542  iscld  21563  clsval2  21586  opncldf1  21620  opncldf2  21621  opncldf3  21622  indiscld  21627  mretopd  21628  restcld  21708  lecldbas  21755  pnrmopn  21879  hauscmplem  21942  elpt  22108  elptr  22109  cfinfil  22429  csdfil  22430  ufilss  22441  filufint  22456  cfinufil  22464  ufinffr  22465  ufilen  22466  prdsxmslem2  23066  lebnumlem1  23492  bcth3  23861  ismbl  24054  ishpg  26472  frgrwopregasn  28022  frgrwopregbsn  28023  disjdifprg  30253  0elsiga  31272  prsiga  31289  sigaclci  31290  difelsiga  31291  unelldsys  31316  sigapildsyslem  31319  sigapildsys  31320  ldgenpisyslem1  31321  isros  31326  unelros  31329  difelros  31330  inelsros  31336  diffiunisros  31337  rossros  31338  elcarsg  31462  ballotlemfval  31646  ballotlemgval  31680  kur14lem1  32350  topdifinffinlem  34510  topdifinffin  34511  dssmapfv3d  40243  dssmapnvod  40244  clsk3nimkb  40268  ntrclsneine0lem  40292  ntrclsk2  40296  ntrclskb  40297  ntrclsk13  40299  ntrclsk4  40300  prsal  42480  saldifcl  42481  salexct  42494  salexct2  42499  salexct3  42502  salgencntex  42503  salgensscntex  42504  caragenel  42654
  Copyright terms: Public domain W3C validator