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

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

Proof of Theorem eleqtrri
StepHypRef Expression
1 eleqtrr.1 . 2 𝐴𝐵
2 eleqtrr.2 . . 3 𝐶 = 𝐵
32eqcomi 2630 . 2 𝐵 = 𝐶
41, 3eleqtri 2696 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wcel 1987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-clel 2617
This theorem is referenced by:  3eltr4i  2711  opi1  4908  opi2  4909  wfrlem14  7388  wfrlem16  7390  seqomlem3  7507  oneo  7621  nnneo  7691  0elixp  7899  ac6sfi  8164  tz9.13  8614  rankval  8639  rankid  8656  ssrankr1  8658  rankel  8662  rankval3  8663  rankpw  8666  rankss  8672  ranksn  8677  rankuni2  8678  rankun  8679  rankpr  8680  rankop  8681  rankeq0  8684  rankr1b  8687  fin1a2lem4  9185  fin1a2lem6  9187  hsmexlem6  9213  dcomex  9229  axdc3lem4  9235  canthp1lem2  9435  pwxpndom2  9447  rankcf  9559  grutsk  9604  axgroth3  9613  inaprc  9618  1lt2pi  9687  pnfxr  10052  mnfxr  10056  1nn  10991  uzrdg0i  12714  axdc4uzlem  12738  ccat2s1p2  13360  wrdl3s3  13655  infcvgaux1i  14533  0bits  15104  sadcf  15118  prmreclem6  15568  xpsfrnel2  16165  setcepi  16678  grpss  17380  psgnunilem2  17855  psgnprfval2  17883  efgi0  18073  efgi1  18074  vrgpf  18121  vrgpinv  18122  frgpuptinv  18124  frgpup2  18129  frgpnabllem1  18216  dmdprdpr  18388  dprdpr  18389  m2detleiblem3  20375  m2detleiblem4  20376  m2detleib  20377  leordtval2  20956  xpstopnlem1  21552  xpstopnlem2  21554  ptcmp  21802  tsmsfbas  21871  zcld  22556  sszcld  22560  abscncfALT  22663  iimulcn  22677  icopnfhmeo  22682  iccpnfhmeo  22684  xrhmeo  22685  cnstrcvs  22881  cncvs  22885  dveflem  23680  ftc1  23743  efopnlem2  24337  cxpcn3  24423  efrlim  24630  structvtxval  25844  usgrexmplef  26078  umgrwwlks2on  26753  konigsberglem4  27017  hhshsslem2  28013  nonbooli  28398  nmopadjlei  28835  fzto1st  29680  xrge0iifhmeo  29806  dya2iocbrsiga  30160  dya2icobrsiga  30161  fib0  30284  fib1  30285  coinflippvt  30369  signstfvn  30468  bnj97  30697  bnj553  30729  bnj966  30775  bnj1442  30878  subfacp1lem2a  30923  subfacp1lem5  30927  erdszelem5  30938  erdszelem8  30941  rankeq1o  31973  0hf  31979  onint1  32143  bj-0eltag  32666  bj-minftyccb  32784  finxpreclem4  32902  fdc  33212  reheibor  33309  pw2f1ocnv  37123  comptiunov2i  37518  corclrcl  37519  clsk1indlem4  37863  clsk1indlem1  37864  sucidALTVD  38628  sucidALT  38629  sucidVD  38630  rfcnpre1  38700  eliuniincex  38816  iocopn  39192  icoopn  39197  islptre  39287  icccncfext  39435  fourierdlem103  39763  fourierdlem104  39764  iooborel  39906  sprsymrelfo  41065  0even  41249  2even  41251  2zrngamgm  41257  zlmodzxzldeplem3  41609
  Copyright terms: Public domain W3C validator