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

Theorem eleqtrri 2913
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 2831 . 2 𝐵 = 𝐶
41, 3eleqtri 2912 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815  df-clel 2894
This theorem is referenced by:  3eltr4i  2927  vex  3472  opi1  5337  opi2  5338  wfrlem14  7955  wfrlem16  7957  seqomlem3  8075  oneo  8194  nnneo  8265  0elixp  8480  ac6sfi  8750  tz9.13  9208  rankval  9233  rankid  9250  ssrankr1  9252  rankel  9256  rankval3  9257  rankpw  9260  rankss  9266  ranksn  9271  rankuni2  9272  rankun  9273  rankpr  9274  rankop  9275  rankeq0  9278  rankr1b  9281  djuun  9343  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  11636  uzrdg0i  13322  axdc4uzlem  13346  ccat2s1p2  13977  ccat2s1p2OLD  13979  wrdl3s3  14317  infcvgaux1i  15203  0bits  15777  sadcf  15791  prmreclem6  16246  fnpr2ob  16822  setcepi  17339  smndex1mnd  18066  smndex1id  18067  pwmnd  18093  grpss  18112  psgnunilem2  18614  psgnprfval2  18642  efgi0  18837  efgi1  18838  vrgpf  18885  vrgpinv  18886  frgpuptinv  18888  frgpup2  18893  frgpnabllem1  18984  dmdprdpr  19162  dprdpr  19163  m2detleiblem3  21232  m2detleiblem4  21233  m2detleib  21234  leordtval2  21815  xpstopnlem1  22412  xpstopnlem2  22414  ptcmp  22661  tsmsfbas  22731  zcld  23416  sszcld  23420  abscncfALT  23527  iimulcn  23541  icopnfhmeo  23546  iccpnfhmeo  23548  xrhmeo  23549  cnstrcvs  23744  cncvs  23748  dveflem  24580  ftc1  24643  efopnlem2  25246  cxpcn3  25335  efrlim  25553  structvtxval  26812  usgrexmplef  27047  wwlks2onv  27737  elwwlks2ons3im  27738  umgrwwlks2on  27741  konigsberglem4  28038  hhshsslem2  29049  nonbooli  29432  nmopadjlei  29869  cshw1s2  30644  fzto1st  30776  cyc2fv1  30794  cyc3fv1  30810  cyc3fv2  30811  cyc3evpm  30823  xrge0iifhmeo  31253  dya2iocbrsiga  31607  dya2icobrsiga  31608  fib0  31731  fib1  31732  coinflippvt  31816  prodfzo03  31948  circlevma  31987  circlemethhgt  31988  hgt750lemg  31999  hgt750lemb  32001  hgt750lema  32002  hgt750leme  32003  tgoldbachgtde  32005  tgoldbachgt  32008  bnj97  32212  bnj553  32244  bnj966  32290  bnj1442  32395  subfacp1lem2a  32501  subfacp1lem5  32505  erdszelem5  32516  erdszelem8  32519  ex-sategoelel12  32748  frrlem14  33210  rankeq1o  33706  0hf  33712  onint1  33871  bj-0eltag  34375  bj-minftyccb  34601  finxpreclem4  34772  fdc  35141  reheibor  35235  0prjspnlem  39542  0prjspnrel  39543  pw2f1ocnv  39908  comptiunov2i  40337  clsk1indlem4  40680  clsk1indlem1  40681  mnuprdlem3  40916  sucidALTVD  41510  sucidALT  41511  sucidVD  41512  rfcnpre1  41582  eliuniincex  41681  iocopn  42096  icoopn  42101  islptre  42200  cnrefiisplem  42410  icccncfext  42468  fourierdlem103  42790  fourierdlem104  42791  iooborel  42930  sprsymrelfo  43953  sbgoldbo  44244  0even  44494  2even  44496  2zrngamgm  44502  zlmodzxzldeplem3  44850  rrx2pxel  45064  rrx2pyel  45065  rrx2linesl  45096  2sphere0  45103
  Copyright terms: Public domain W3C validator