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

Theorem syl5eleqr 2476
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eleqr.1  |-  A  e.  B
syl5eleqr.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
syl5eleqr  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl5eleqr
StepHypRef Expression
1 syl5eleqr.1 . 2  |-  A  e.  B
2 syl5eleqr.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2394 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2475 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717
This theorem is referenced by:  rabsnt  3826  reusv6OLD  4676  onnev  4900  opabiota  6476  canth  6477  onnseq  6544  tfrlem16  6592  oen0  6767  nnawordex  6818  inf0  7511  cantnflt  7562  cnfcom2  7594  cnfcom3lem  7595  cnfcom3  7596  r1ordg  7639  r1val1  7647  rankr1id  7723  acacni  7955  dfacacn  7956  dfac13  7957  cda1dif  7991  ttukeylem5  8328  ttukeylem6  8329  gchac  8483  gch2  8489  gch3  8490  gchina  8509  swrds1  11716  sadcp1  12896  xpsfrnel2  13719  idfucl  14007  gsumz  14710  gsumval2  14712  frmdmnd  14733  frmd0  14734  efginvrel2  15288  efgcpbl2  15318  pgpfaclem1  15568  lbsexg  16165  dfac14  17573  acufl  17872  cnextfvval  18019  cnextcn  18021  minveclem3b  19198  minveclem4a  19200  ovollb2  19254  ovolunlem1a  19261  ovolunlem1  19262  ovoliunlem1  19267  ovoliun2  19271  ioombl1lem4  19324  uniioombllem1  19342  uniioombllem2  19344  uniioombllem6  19349  itg2monolem1  19511  itg2mono  19514  itg2cnlem1  19522  xrlimcnp  20676  efrlim  20677  cusgrares  21349  usgrcyclnl1  21477  ex-br  21589  vcoprne  21908  rge0scvg  24141  topjoin  26087  aomclem1  26822  dfac21  26835  frlmlbs  26920  pclfinN  30016
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2382  df-clel 2385
  Copyright terms: Public domain W3C validator