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

Theorem difeq1 4078
Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
difeq1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem difeq1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 rabeq 3469 . 2 (𝐴 = 𝐵 → {𝑥𝐴 ∣ ¬ 𝑥𝐶} = {𝑥𝐵 ∣ ¬ 𝑥𝐶})
2 dfdif2 3928 . 2 (𝐴𝐶) = {𝑥𝐴 ∣ ¬ 𝑥𝐶}
3 dfdif2 3928 . 2 (𝐵𝐶) = {𝑥𝐵 ∣ ¬ 𝑥𝐶}
41, 2, 33eqtr4g 2884 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wcel 2115  {crab 3137  cdif 3916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-dif 3922
This theorem is referenced by:  difeq12  4080  difeq1i  4081  difeq1d  4084  symdifeq1  4206  uneqdifeq  4421  hartogslem1  9003  kmlem9  9582  kmlem11  9584  kmlem12  9585  isfin1a  9712  fin1a2lem13  9832  fundmge2nop0  13855  incexclem  15191  coprmprod  16003  coprmproddvds  16005  ismri  16902  f1otrspeq  18575  pmtrval  18579  pmtrfrn  18586  symgsssg  18595  symgfisg  18596  symggen  18598  psgnunilem1  18621  psgnunilem5  18622  psgneldm  18631  ablfac1eulem  19194  sdrgacs  19580  islbs  19848  lbsextlem1  19930  lbsextlem2  19931  lbsextlem3  19932  lbsextlem4  19933  cofipsgn  20339  selvffval  20795  submafval  21191  m1detdiag  21209  lpval  21750  2ndcdisj  22067  isufil  22514  ptcmplem2  22664  mblsplit  24142  voliunlem3  24162  ig1pval  24779  nbgr2vtx1edg  27146  nbuhgr2vtx1edgb  27148  nbgr0vtx  27152  nb3grprlem2  27177  uvtx01vtx  27193  cplgr1v  27226  dfconngr1  27979  isconngr1  27981  isfrgr  28051  frgr1v  28062  nfrgr2v  28063  frgr3v  28066  1vwmgr  28067  3vfriswmgr  28069  difeq  30294  symgcntz  30764  tocycval  30785  sigaval  31430  issiga  31431  issgon  31442  isros  31487  unelros  31490  difelros  31491  inelsros  31497  diffiunisros  31498  rossros  31499  inelcarsg  31629  carsgclctunlem2  31637  probun  31737  ballotlemgval  31841  cvmscbv  32565  cvmsi  32572  cvmsval  32573  poimirlem4  35009  dssmapfvd  40639  compne  41069  dvmptfprod  42517  caragensplit  43069  vonvolmbllem  43229  vonvolmbl  43230  ldepsnlinc  44847  eenglngeehlnm  45083
  Copyright terms: Public domain W3C validator