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

Theorem eleqtrri 2369
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eleqtrr.1  |-  A  e.  B
eleqtrr.2  |-  C  =  B
Assertion
Ref Expression
eleqtrri  |-  A  e.  C

Proof of Theorem eleqtrri
StepHypRef Expression
1 eleqtrr.1 . 2  |-  A  e.  B
2 eleqtrr.2 . . 3  |-  C  =  B
32eqcomi 2300 . 2  |-  B  =  C
41, 3eleqtri 2368 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696
This theorem is referenced by:  3eltr4i  2375  opi1  4256  opi2  4257  seqomlem3  6480  oneo  6595  nnneo  6665  0elixp  6863  ac6sfi  7117  oancom  7368  tz9.13  7479  rankval  7504  rankid  7521  ssrankr1  7523  rankel  7527  rankval3  7528  rankpw  7531  rankss  7537  ranksn  7542  rankuni2  7543  rankun  7544  rankpr  7545  rankop  7546  rankeq0  7549  rankr1b  7552  fin1a2lem4  8045  fin1a2lem6  8047  hsmexlem6  8073  dcomex  8089  axdc3lem4  8095  canthp1lem2  8291  pwxpndom2  8303  rankcf  8415  grutsk  8460  axgroth3  8469  inaprc  8474  1lt2pi  8545  1nn  9773  pnfxr  10471  mnfxr  10472  uzrdg0i  11038  axdc4uzlem  11060  eqs1  11463  infcvgaux1i  12331  0bits  12646  sadcf  12660  prmreclem6  12984  xpsfrnel2  13483  setcepi  13936  grpss  14519  efgi0  15045  efgi1  15046  vrgpf  15093  vrgpinv  15094  frgpuptinv  15096  frgpup2  15101  frgpnabllem1  15177  dmdprdpr  15300  dprdpr  15301  leordtval2  16958  xpstopnlem1  17516  xpstopnlem2  17518  ptcmp  17768  tsmsfbas  17826  zcld  18335  abscncfALT  18439  iimulcn  18452  icopnfhmeo  18457  iccpnfhmeo  18459  xrhmeo  18460  dveflem  19342  ftc1  19405  efopnlem2  20020  cxpcn3  20104  efrlim  20280  hhshsslem2  21861  nonbooli  22246  nmopadjlei  22684  xrge0iifhmeo  23333  lmxrge0  23390  dya2iocbrsiga  23593  coinflippvt  23700  subfacp1lem2a  23726  subfacp1lem5  23730  erdszelem5  23741  erdszelem8  23744  konigsberg  23926  sinccvglem  24020  wfrlem14  24340  wfrlem16  24342  rankeq1o  24873  0hf  24879  onint1  24960  dominc  25383  rninc  25384  cinei  25726  1ded  25841  empklst  26112  pgapspf  26155  fdc  26558  reheibor  26666  pw2f1ocnv  27233  psgnunilem2  27521  rfcnpre1  27793  usgraex0elv  28262  usgraex1elv  28263  usgraex2elv  28264  usgraex3elv  28265  wlkntrllem1  28345  sucidALTVD  28962  sucidALT  28963  sucidVD  28964  bnj97  29214  bnj553  29246  bnj966  29292  bnj1442  29395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator