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

Theorem eleqtrri 2729
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 2660 . 2 𝐵 = 𝐶
41, 3eleqtri 2728 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  3eltr4i  2743  opi1  4966  opi2  4967  wfrlem14  7473  wfrlem16  7475  seqomlem3  7592  oneo  7706  nnneo  7776  0elixp  7981  ac6sfi  8245  tz9.13  8692  rankval  8717  rankid  8734  ssrankr1  8736  rankel  8740  rankval3  8741  rankpw  8744  rankss  8750  ranksn  8755  rankuni2  8756  rankun  8757  rankpr  8758  rankop  8759  rankeq0  8762  rankr1b  8765  fin1a2lem4  9263  fin1a2lem6  9265  hsmexlem6  9291  dcomex  9307  axdc3lem4  9313  canthp1lem2  9513  pwxpndom2  9525  rankcf  9637  grutsk  9682  axgroth3  9691  inaprc  9696  1lt2pi  9765  pnfxr  10130  mnfxr  10134  1nn  11069  uzrdg0i  12798  axdc4uzlem  12822  ccat2s1p2  13450  wrdl3s3  13751  infcvgaux1i  14633  0bits  15208  sadcf  15222  prmreclem6  15672  xpsfrnel2  16272  setcepi  16785  grpss  17487  psgnunilem2  17961  psgnprfval2  17989  efgi0  18179  efgi1  18180  vrgpf  18227  vrgpinv  18228  frgpuptinv  18230  frgpup2  18235  frgpnabllem1  18322  dmdprdpr  18494  dprdpr  18495  m2detleiblem3  20483  m2detleiblem4  20484  m2detleib  20485  leordtval2  21064  xpstopnlem1  21660  xpstopnlem2  21662  ptcmp  21909  tsmsfbas  21978  zcld  22663  sszcld  22667  abscncfALT  22770  iimulcn  22784  icopnfhmeo  22789  iccpnfhmeo  22791  xrhmeo  22792  cnstrcvs  22987  cncvs  22991  dveflem  23787  ftc1  23850  efopnlem2  24448  cxpcn3  24534  efrlim  24741  structvtxval  25955  usgrexmplef  26196  wwlks2onv  26918  elwwlks2ons3im  26919  umgrwwlks2on  26923  konigsberglem4  27233  2clwwlk2clwwlklem2lem2  27329  hhshsslem2  28253  nonbooli  28638  nmopadjlei  29075  fzto1st  29981  xrge0iifhmeo  30110  dya2iocbrsiga  30465  dya2icobrsiga  30466  fib0  30589  fib1  30590  coinflippvt  30674  signstfvn  30774  prodfzo03  30809  circlevma  30848  circlemethhgt  30849  hgt750lemg  30860  hgt750lemb  30862  hgt750lema  30863  hgt750leme  30864  tgoldbachgtde  30866  tgoldbachgt  30869  bnj97  31062  bnj553  31094  bnj966  31140  bnj1442  31243  subfacp1lem2a  31288  subfacp1lem5  31292  erdszelem5  31303  erdszelem8  31306  rankeq1o  32403  0hf  32409  onint1  32573  bj-0eltag  33091  bj-minftyccb  33242  finxpreclem4  33361  fdc  33671  reheibor  33768  pw2f1ocnv  37921  comptiunov2i  38315  corclrcl  38316  clsk1indlem4  38659  clsk1indlem1  38660  sucidALTVD  39420  sucidALT  39421  sucidVD  39422  rfcnpre1  39492  eliuniincex  39606  iocopn  40064  icoopn  40069  islptre  40169  cnrefiisplem  40373  icccncfext  40418  fourierdlem103  40744  fourierdlem104  40745  iooborel  40887  sbgoldbo  42000  sprsymrelfo  42072  0even  42256  2even  42258  2zrngamgm  42264  zlmodzxzldeplem3  42616
  Copyright terms: Public domain W3C validator