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

Theorem syl5eleqr 2491
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 2409 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2490 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721
This theorem is referenced by:  rabsnt  3841  reusv6OLD  4693  onnev  4917  opabiota  6497  canth  6498  onnseq  6565  tfrlem16  6613  oen0  6788  nnawordex  6839  inf0  7532  cantnflt  7583  cnfcom2  7615  cnfcom3lem  7616  cnfcom3  7617  r1ordg  7660  r1val1  7668  rankr1id  7744  acacni  7976  dfacacn  7977  dfac13  7978  cda1dif  8012  ttukeylem5  8349  ttukeylem6  8350  gchac  8504  gch2  8510  gch3  8511  gchina  8530  swrds1  11742  sadcp1  12922  xpsfrnel2  13745  idfucl  14033  gsumz  14736  gsumval2  14738  frmdmnd  14759  frmd0  14760  efginvrel2  15314  efgcpbl2  15344  pgpfaclem1  15594  lbsexg  16191  dfac14  17603  acufl  17902  cnextfvval  18049  cnextcn  18051  minveclem3b  19282  minveclem4a  19284  ovollb2  19338  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliun2  19355  ioombl1lem4  19408  uniioombllem1  19426  uniioombllem2  19428  uniioombllem6  19433  itg2monolem1  19595  itg2mono  19598  itg2cnlem1  19606  xrlimcnp  20760  efrlim  20761  cusgrares  21434  usgrcyclnl1  21580  ex-br  21692  vcoprne  22011  rge0scvg  24288  topjoin  26284  aomclem1  27019  dfac21  27032  frlmlbs  27117  pclfinN  30382
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 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator