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

Theorem difeq2 4081
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 2827 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21notbid 318 . . 3 (𝐴 = 𝐵 → (¬ 𝑥𝐴 ↔ ¬ 𝑥𝐵))
32rabbidv 3418 . 2 (𝐴 = 𝐵 → {𝑥𝐶 ∣ ¬ 𝑥𝐴} = {𝑥𝐶 ∣ ¬ 𝑥𝐵})
4 dfdif2 3924 . 2 (𝐶𝐴) = {𝑥𝐶 ∣ ¬ 𝑥𝐴}
5 dfdif2 3924 . 2 (𝐶𝐵) = {𝑥𝐶 ∣ ¬ 𝑥𝐵}
63, 4, 53eqtr4g 2802 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wcel 2107  {crab 3410  cdif 3912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-dif 3918
This theorem is referenced by:  difeq12  4082  difeq2i  4084  difeq2d  4087  symdifeq1  4209  ssdifim  4227  disjdif2  4444  ssdifeq0  4449  sorpsscmpl  7676  2oconcl  8454  oev  8465  sbthlem2  9035  sbth  9044  sbthfi  9153  infdiffi  9601  fin1ai  10236  fin23lem7  10259  fin23lem11  10260  compsscnv  10314  isf34lem1  10315  compss  10319  isf34lem4  10320  fin1a2lem7  10349  pwfseqlem4a  10604  pwfseqlem4  10605  efgmval  19501  efgi  19508  frgpuptinv  19560  gsumcllem  19692  gsumzaddlem  19705  selvfval  21543  fctop  22370  cctop  22372  iscld  22394  clsval2  22417  opncldf1  22451  opncldf2  22452  opncldf3  22453  indiscld  22458  mretopd  22459  restcld  22539  lecldbas  22586  pnrmopn  22710  hauscmplem  22773  elpt  22939  elptr  22940  cfinfil  23260  csdfil  23261  ufilss  23272  filufint  23287  cfinufil  23295  ufinffr  23296  ufilen  23297  prdsxmslem2  23901  lebnumlem1  24340  bcth3  24711  ismbl  24906  ishpg  27743  frgrwopregasn  29302  frgrwopregbsn  29303  disjdifprg  31535  0elsiga  32753  prsiga  32770  sigaclci  32771  difelsiga  32772  unelldsys  32797  sigapildsyslem  32800  sigapildsys  32801  ldgenpisyslem1  32802  isros  32807  unelros  32810  difelros  32811  inelsros  32817  diffiunisros  32818  rossros  32819  elcarsg  32945  ballotlemfval  33129  ballotlemgval  33163  kur14lem1  33840  topdifinffinlem  35847  topdifinffin  35848  oe0rif  41649  dssmapfv3d  42365  dssmapnvod  42366  clsk3nimkb  42386  ntrclsneine0lem  42410  ntrclsk2  42414  ntrclskb  42415  ntrclsk13  42417  ntrclsk4  42418  prsal  44633  saldifcl  44634  salexct  44649  salexct2  44654  salexct3  44657  salgencntex  44658  salgensscntex  44659  caragenel  44810  opncldeqv  47008
  Copyright terms: Public domain W3C validator