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

Theorem eleqtrri 2883
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 2814 . 2 𝐵 = 𝐶
41, 3eleqtri 2882 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wcel 2158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2798  df-clel 2801
This theorem is referenced by:  3eltr4i  2897  opi1  5123  opi2  5124  wfrlem14  7661  wfrlem16  7663  seqomlem3  7780  oneo  7895  nnneo  7965  0elixp  8173  ac6sfi  8440  tz9.13  8898  rankval  8923  rankid  8940  ssrankr1  8942  rankel  8946  rankval3  8947  rankpw  8950  rankss  8956  ranksn  8961  rankuni2  8962  rankun  8963  rankpr  8964  rankop  8965  rankeq0  8968  rankr1b  8971  djuun  9032  fin1a2lem4  9507  fin1a2lem6  9509  hsmexlem6  9535  dcomex  9551  axdc3lem4  9557  canthp1lem2  9757  pwxpndom2  9769  rankcf  9881  grutsk  9926  axgroth3  9935  inaprc  9940  1lt2pi  10009  pnfxr  10374  mnfxr  10378  1nn  11313  uzrdg0i  12978  axdc4uzlem  13002  ccat2s1p2  13624  wrdl3s3  13926  infcvgaux1i  14807  0bits  15376  sadcf  15390  prmreclem6  15838  xpsfrnel2  16426  setcepi  16938  grpss  17641  psgnunilem2  18112  psgnprfval2  18140  efgi0  18330  efgi1  18331  vrgpf  18378  vrgpinv  18379  frgpuptinv  18381  frgpup2  18386  frgpnabllem1  18473  dmdprdpr  18646  dprdpr  18647  m2detleiblem3  20642  m2detleiblem4  20643  m2detleib  20644  leordtval2  21226  xpstopnlem1  21822  xpstopnlem2  21824  ptcmp  22071  tsmsfbas  22140  zcld  22825  sszcld  22829  abscncfALT  22932  iimulcn  22946  icopnfhmeo  22951  iccpnfhmeo  22953  xrhmeo  22954  cnstrcvs  23149  cncvs  23153  dveflem  23952  ftc1  24015  efopnlem2  24613  cxpcn3  24699  efrlim  24906  structvtxval  26120  usgrexmplef  26363  wwlks2onv  27089  elwwlks2ons3im  27090  umgrwwlks2on  27094  konigsberglem4  27424  hhshsslem2  28450  nonbooli  28835  nmopadjlei  29272  fzto1st  30175  xrge0iifhmeo  30304  dya2iocbrsiga  30659  dya2icobrsiga  30660  fib0  30783  fib1  30784  coinflippvt  30868  signstfvn  30968  prodfzo03  31003  circlevma  31042  circlemethhgt  31043  hgt750lemg  31054  hgt750lemb  31056  hgt750lema  31057  hgt750leme  31058  tgoldbachgtde  31060  tgoldbachgt  31063  bnj97  31256  bnj553  31288  bnj966  31334  bnj1442  31437  subfacp1lem2a  31482  subfacp1lem5  31486  erdszelem5  31497  erdszelem8  31500  rankeq1o  32596  0hf  32602  onint1  32762  bj-0eltag  33273  bj-minftyccb  33426  finxpreclem4  33544  cnfin0  33553  fdc  33849  reheibor  33946  pw2f1ocnv  38102  comptiunov2i  38495  corclrcl  38496  clsk1indlem4  38839  clsk1indlem1  38840  sucidALTVD  39597  sucidALT  39598  sucidVD  39599  rfcnpre1  39669  eliuniincex  39781  iocopn  40224  icoopn  40229  islptre  40328  cnrefiisplem  40532  icccncfext  40577  fourierdlem103  40902  fourierdlem104  40903  iooborel  41045  sbgoldbo  42247  sprsymrelfo  42312  0even  42496  2even  42498  2zrngamgm  42504  zlmodzxzldeplem3  42856
  Copyright terms: Public domain W3C validator