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

Theorem eleqtrri 2683
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 2615 . 2 𝐵 = 𝐶
41, 3eleqtri 2682 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2599  df-clel 2602
This theorem is referenced by:  3eltr4i  2697  opi1  4855  opi2  4856  wfrlem14  7289  wfrlem16  7291  seqomlem3  7408  oneo  7522  nnneo  7592  0elixp  7799  ac6sfi  8063  tz9.13  8511  rankval  8536  rankid  8553  ssrankr1  8555  rankel  8559  rankval3  8560  rankpw  8563  rankss  8569  ranksn  8574  rankuni2  8575  rankun  8576  rankpr  8577  rankop  8578  rankeq0  8581  rankr1b  8584  fin1a2lem4  9082  fin1a2lem6  9084  hsmexlem6  9110  dcomex  9126  axdc3lem4  9132  canthp1lem2  9328  pwxpndom2  9340  rankcf  9452  grutsk  9497  axgroth3  9506  inaprc  9511  1lt2pi  9580  1nn  10875  pnfxr  11778  mnfxr  11780  uzrdg0i  12572  axdc4uzlem  12596  ccat2s1p2  13201  wrdl3s3  13496  infcvgaux1i  14371  0bits  14942  sadcf  14956  prmreclem6  15406  xpsfrnel2  15991  setcepi  16504  grpss  17206  psgnunilem2  17681  psgnprfval2  17709  efgi0  17899  efgi1  17900  vrgpf  17947  vrgpinv  17948  frgpuptinv  17950  frgpup2  17955  frgpnabllem1  18042  dmdprdpr  18214  dprdpr  18215  m2detleiblem3  20193  m2detleiblem4  20194  m2detleib  20195  leordtval2  20765  xpstopnlem1  21361  xpstopnlem2  21363  ptcmp  21611  tsmsfbas  21680  zcld  22353  sszcld  22357  abscncfALT  22459  iimulcn  22473  icopnfhmeo  22478  iccpnfhmeo  22480  xrhmeo  22481  cnstrcvs  22675  cncvs  22679  dveflem  23460  ftc1  23523  efopnlem2  24117  cxpcn3  24203  efrlim  24410  usgraex0elv  25687  usgraex1elv  25688  usgraex2elv  25689  usgraex3elv  25690  wlkntrllem1  25852  usgra2adedgwlkonALT  25907  usgra2wlkspthlem2  25911  el2wlkonotlem  26152  usg2wlkonot  26173  usg2wotspth  26174  konigsberg  26277  hhshsslem2  27312  nonbooli  27697  nmopadjlei  28134  fzto1st  28987  xrge0iifhmeo  29113  dya2iocbrsiga  29467  dya2icobrsiga  29468  fib0  29591  fib1  29592  coinflippvt  29676  signstfvn  29775  bnj97  29993  bnj553  30025  bnj966  30071  bnj1442  30174  subfacp1lem2a  30219  subfacp1lem5  30223  erdszelem5  30234  erdszelem8  30237  rankeq1o  31251  0hf  31257  onint1  31421  bj-0eltag  31959  bj-minftyccb  32089  finxpreclem4  32207  fdc  32511  reheibor  32608  pw2f1ocnv  36422  comptiunov2i  36817  corclrcl  36818  clsk1indlem4  37162  clsk1indlem1  37163  sucidALTVD  37928  sucidALT  37929  sucidVD  37930  rfcnpre1  38001  eliuniincex  38123  iocopn  38394  icoopn  38399  islptre  38487  icccncfext  38574  fourierdlem103  38903  fourierdlem104  38904  iooborel  39046  umgrwwlks2on  41160  konigsberglem4  41424  0even  41720  2even  41722  2zrngamgm  41728  zlmodzxzldeplem3  42084
  Copyright terms: Public domain W3C validator