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

Theorem eleqtrri 2544
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 2470 . 2
41, 3eleqtri 2543 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818
This theorem is referenced by:  3eltr4i  2558  opi1  4719  opi2  4720  seqomlem3  7136  oneo  7249  nnneo  7319  0elixp  7520  ac6sfi  7784  tz9.13  8230  rankval  8255  rankid  8272  ssrankr1  8274  rankel  8278  rankval3  8279  rankpw  8282  rankss  8288  ranksn  8293  rankuni2  8294  rankun  8295  rankpr  8296  rankop  8297  rankeq0  8300  rankr1b  8303  fin1a2lem4  8804  fin1a2lem6  8806  hsmexlem6  8832  dcomex  8848  axdc3lem4  8854  canthp1lem2  9052  pwxpndom2  9064  rankcf  9176  grutsk  9221  axgroth3  9230  inaprc  9235  1lt2pi  9304  1nn  10572  pnfxr  11350  mnfxr  11352  uzrdg0i  12070  axdc4uzlem  12092  eqs1  12621  ccat2s1p2  12633  infcvgaux1i  13668  0bits  14089  sadcf  14103  prmreclem6  14439  xpsfrnel2  14962  setcepi  15415  grpss  16071  psgnunilem2  16520  psgnprfval2  16548  efgi0  16738  efgi1  16739  vrgpf  16786  vrgpinv  16787  frgpuptinv  16789  frgpup2  16794  frgpnabllem1  16877  dmdprdpr  17098  dprdpr  17099  m2detleiblem3  19131  m2detleiblem4  19132  m2detleib  19133  leordtval2  19713  xpstopnlem1  20310  xpstopnlem2  20312  ptcmp  20558  tsmsfbas  20626  zcld  21318  sszcld  21322  abscncfALT  21424  iimulcn  21438  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  dveflem  22380  ftc1  22443  efopnlem2  23038  cxpcn3  23122  efrlim  23299  usgraex0elv  24396  usgraex1elv  24397  usgraex2elv  24398  usgraex3elv  24399  wlkntrllem1  24561  usgra2adedgwlkonALT  24616  usgra2wlkspthlem2  24620  el2wlkonotlem  24862  usg2wlkonot  24883  usg2wotspth  24884  konigsberg  24987  hhshsslem2  26184  nonbooli  26569  nmopadjlei  27007  xrge0iifhmeo  27918  dya2iocbrsiga  28246  dya2icobrsiga  28247  fib0  28338  fib1  28339  coinflippvt  28423  signstfvn  28526  subfacp1lem2a  28624  subfacp1lem5  28628  erdszelem5  28639  erdszelem8  28642  wfrlem14  29356  wfrlem16  29358  rankeq1o  29828  0hf  29834  onint1  29914  fdc  30238  reheibor  30335  pw2f1ocnv  30979  rfcnpre1  31394  iocopn  31560  icoopn  31565  islptre  31625  icccncfext  31690  fourierdlem103  31992  fourierdlem104  31993  usgra2pthspth  32351  0even  32737  2even  32739  2zrngamgm  32745  zlmodzxzldeplem3  33103  sucidALTVD  33670  sucidALT  33671  sucidVD  33672  bnj97  33924  bnj553  33956  bnj966  34002  bnj1442  34105  bj-0eltag  34536  bj-minftyccb  34628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator