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

Theorem difeq1 3587
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 3070 . 2 (𝐴 = 𝐵 → {𝑥𝐴 ∣ ¬ 𝑥𝐶} = {𝑥𝐵 ∣ ¬ 𝑥𝐶})
2 dfdif2 3453 . 2 (𝐴𝐶) = {𝑥𝐴 ∣ ¬ 𝑥𝐶}
3 dfdif2 3453 . 2 (𝐵𝐶) = {𝑥𝐵 ∣ ¬ 𝑥𝐶}
41, 2, 33eqtr4g 2573 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wcel 1938  {crab 2804  cdif 3441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rab 2809  df-dif 3447
This theorem is referenced by:  difeq12  3589  difeq1i  3590  difeq1d  3593  symdifeq1  3711  uneqdifeq  3912  uneqdifeqOLD  3913  hartogslem1  8206  kmlem9  8739  kmlem11  8741  kmlem12  8742  isfin1a  8873  fin1a2lem13  8993  incexclem  14276  coprmprod  15089  coprmproddvds  15091  ismri  16006  f1otrspeq  17582  pmtrval  17586  pmtrfrn  17593  symgsssg  17602  symgfisg  17603  symggen  17605  psgnunilem1  17628  psgnunilem5  17629  psgneldm  17638  ablfac1eulem  18201  islbs  18801  lbsextlem1  18883  lbsextlem2  18884  lbsextlem3  18885  lbsextlem4  18886  zrhcofipsgn  19664  submafval  20107  m1detdiag  20125  lpval  20656  2ndcdisj  20972  isufil  21420  ptcmplem2  21570  mblsplit  22982  voliunlem3  23002  ig1pval  23614  ig1pvalOLD  23620  nb3graprlem2  25719  iscusgra  25723  isuvtx  25754  isfrgra  26255  1vwmgra  26268  3vfriswmgra  26270  difeq  28527  sigaval  29296  issiga  29297  issgon  29309  isros  29354  unelros  29357  difelros  29358  inelsros  29364  diffiunisros  29365  rossros  29366  inelcarsg  29506  carsgclctunlem2  29514  probun  29615  ballotlemgval  29719  ballotlemgvalOLD  29757  cvmscbv  30339  cvmsi  30346  cvmsval  30347  poimirlem4  32473  sdrgacs  36687  dssmapfvd  37228  compne  37562  dvmptfprod  38738  caragensplit  39297  vonvolmbllem  39457  vonvolmbl  39458  fundmge2nop0  40255  nbgr2vtx1edg  40677  nbuhgr2vtx1edgb  40679  nbgr0vtx  40683  nb3grprlem2  40714  uvtxa01vtx0  40728  cplgr1v  40757  dfconngr1  41460  isconngr1  41462  isfrgr  41535  frgr1v  41546  nfrgr2v  41547  frgr3v  41550  1vwmgr  41551  3vfriswmgr  41553  ldepsnlinc  42196
  Copyright terms: Public domain W3C validator