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

Theorem eleqtrri 2511
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 2442 . 2  |-  B  =  C
41, 3eleqtri 2510 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1726
This theorem is referenced by:  3eltr4i  2517  opi1  4432  opi2  4433  seqomlem3  6711  oneo  6826  nnneo  6896  0elixp  7095  ac6sfi  7353  tz9.13  7719  rankval  7744  rankid  7761  ssrankr1  7763  rankel  7767  rankval3  7768  rankpw  7771  rankss  7777  ranksn  7782  rankuni2  7783  rankun  7784  rankpr  7785  rankop  7786  rankeq0  7789  rankr1b  7792  fin1a2lem4  8285  fin1a2lem6  8287  hsmexlem6  8313  dcomex  8329  axdc3lem4  8335  canthp1lem2  8530  pwxpndom2  8542  rankcf  8654  grutsk  8699  axgroth3  8708  inaprc  8713  1lt2pi  8784  1nn  10013  pnfxr  10715  mnfxr  10716  uzrdg0i  11301  axdc4uzlem  11323  eqs1  11763  infcvgaux1i  12638  0bits  12953  sadcf  12967  prmreclem6  13291  xpsfrnel2  13792  setcepi  14245  grpss  14828  efgi0  15354  efgi1  15355  vrgpf  15402  vrgpinv  15403  frgpuptinv  15405  frgpup2  15410  frgpnabllem1  15486  dmdprdpr  15609  dprdpr  15610  leordtval2  17278  xpstopnlem1  17843  xpstopnlem2  17845  ptcmp  18091  tsmsfbas  18159  zcld  18846  sszcld  18850  abscncfALT  18952  iimulcn  18965  icopnfhmeo  18970  iccpnfhmeo  18972  xrhmeo  18973  dveflem  19865  ftc1  19928  efopnlem2  20550  cxpcn3  20634  efrlim  20810  usgraex0elv  21417  usgraex1elv  21418  usgraex2elv  21419  usgraex3elv  21420  wlkntrllem1  21561  konigsberg  21711  hhshsslem2  22770  nonbooli  23155  nmopadjlei  23593  xrge0iifhmeo  24324  dya2iocbrsiga  24627  dya2icobrsiga  24628  coinflippvt  24744  subfacp1lem2a  24868  subfacp1lem5  24872  erdszelem5  24883  erdszelem8  24886  wfrlem14  25553  wfrlem16  25555  rankeq1o  26114  0hf  26120  onint1  26201  fdc  26451  reheibor  26550  pw2f1ocnv  27110  psgnunilem2  27397  rfcnpre1  27668  usgra2pthspth  28331  usgra2wlkspthlem2  28333  el2wlkonotlem  28382  usg2wlkonot  28403  usg2wotspth  28404  sucidALTVD  29044  sucidALT  29045  sucidVD  29046  bnj97  29299  bnj553  29331  bnj966  29377  bnj1442  29480
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-clel 2434
  Copyright terms: Public domain W3C validator