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

Theorem eleqtrri 2912
Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)
Hypotheses
Ref Expression
eleqtrri.1 𝐴𝐵
eleqtrri.2 𝐶 = 𝐵
Assertion
Ref Expression
eleqtrri 𝐴𝐶

Proof of Theorem eleqtrri
StepHypRef Expression
1 eleqtrri.1 . 2 𝐴𝐵
2 eleqtrri.2 . . 3 𝐶 = 𝐵
32eqcomi 2830 . 2 𝐵 = 𝐶
41, 3eleqtri 2911 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893
This theorem is referenced by:  3eltr4i  2926  vex  3498  opi1  5352  opi2  5353  wfrlem14  7959  wfrlem16  7961  seqomlem3  8079  oneo  8197  nnneo  8268  0elixp  8482  ac6sfi  8751  tz9.13  9209  rankval  9234  rankid  9251  ssrankr1  9253  rankel  9257  rankval3  9258  rankpw  9261  rankss  9267  ranksn  9272  rankuni2  9273  rankun  9274  rankpr  9275  rankop  9276  rankeq0  9279  rankr1b  9282  djuun  9344  dju1dif  9587  isfin4p1  9726  fin1a2lem4  9814  fin1a2lem6  9816  hsmexlem6  9842  dcomex  9858  axdc3lem4  9864  canthp1lem2  10064  pwxpndom2  10076  rankcf  10188  grutsk  10233  axgroth3  10242  inaprc  10247  1lt2pi  10316  pnfxr  10684  mnfxr  10687  1nn  11638  uzrdg0i  13317  axdc4uzlem  13341  ccat2s1p2  13976  ccat2s1p2OLD  13978  wrdl3s3  14316  infcvgaux1i  15202  0bits  15778  sadcf  15792  prmreclem6  16247  fnpr2ob  16821  setcepi  17338  pwmnd  18042  grpss  18061  psgnunilem2  18554  psgnprfval2  18582  efgi0  18777  efgi1  18778  vrgpf  18825  vrgpinv  18826  frgpuptinv  18828  frgpup2  18833  frgpnabllem1  18924  dmdprdpr  19102  dprdpr  19103  m2detleiblem3  21168  m2detleiblem4  21169  m2detleib  21170  leordtval2  21750  xpstopnlem1  22347  xpstopnlem2  22349  ptcmp  22596  tsmsfbas  22665  zcld  23350  sszcld  23354  abscncfALT  23457  iimulcn  23471  icopnfhmeo  23476  iccpnfhmeo  23478  xrhmeo  23479  cnstrcvs  23674  cncvs  23678  dveflem  24505  ftc1  24568  efopnlem2  25167  cxpcn3  25256  efrlim  25475  structvtxval  26734  usgrexmplef  26969  wwlks2onv  27660  elwwlks2ons3im  27661  umgrwwlks2on  27664  konigsberglem4  27962  hhshsslem2  28973  nonbooli  29356  nmopadjlei  29793  cshw1s2  30562  fzto1st  30673  cyc2fv1  30691  cyc3fv1  30707  cyc3fv2  30708  cyc3evpm  30720  xrge0iifhmeo  31079  dya2iocbrsiga  31433  dya2icobrsiga  31434  fib0  31557  fib1  31558  coinflippvt  31642  prodfzo03  31774  circlevma  31813  circlemethhgt  31814  hgt750lemg  31825  hgt750lemb  31827  hgt750lema  31828  hgt750leme  31829  tgoldbachgtde  31831  tgoldbachgt  31834  bnj97  32038  bnj553  32070  bnj966  32116  bnj1442  32219  subfacp1lem2a  32325  subfacp1lem5  32329  erdszelem5  32340  erdszelem8  32343  ex-sategoelel12  32572  frrlem14  33034  rankeq1o  33530  0hf  33536  onint1  33695  bj-0eltag  34188  bj-minftyccb  34400  finxpreclem4  34558  fdc  34903  reheibor  35000  0prjspnlem  39148  0prjspnrel  39149  pw2f1ocnv  39514  comptiunov2i  39931  clsk1indlem4  40274  clsk1indlem1  40275  mnuprdlem3  40490  sucidALTVD  41084  sucidALT  41085  sucidVD  41086  rfcnpre1  41156  eliuniincex  41256  iocopn  41676  icoopn  41681  islptre  41780  cnrefiisplem  41990  icccncfext  42050  fourierdlem103  42375  fourierdlem104  42376  iooborel  42515  sprsymrelfo  43506  sbgoldbo  43799  smndex1mnd  43980  smndex1id  43981  0even  44100  2even  44102  2zrngamgm  44108  zlmodzxzldeplem3  44455  rrx2pxel  44596  rrx2pyel  44597  rrx2linesl  44628  2sphere0  44635
  Copyright terms: Public domain W3C validator