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

Theorem syl5eleqr 2370
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 2288 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2369 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  rabsnt  3704  reusv6OLD  4545  onnev  4770  opabiota  6293  canth  6294  onnseq  6361  tfrlem16  6409  oen0  6584  nnawordex  6635  inf0  7322  cantnflt  7373  cnfcom2  7405  cnfcom3lem  7406  cnfcom3  7407  r1ordg  7450  r1val1  7458  rankr1id  7534  acacni  7766  dfacacn  7767  dfac13  7768  cda1dif  7802  ttukeylem5  8140  ttukeylem6  8141  gchac  8295  gch2  8301  gch3  8302  gchina  8321  swrds1  11473  sadcp1  12646  xpsfrnel2  13467  idfucl  13755  gsumz  14458  gsumval2  14460  frmdmnd  14481  frmd0  14482  efginvrel2  15036  efgcpbl2  15066  pgpfaclem1  15316  lbsexg  15917  dfac14  17312  acufl  17612  minveclem3b  18792  minveclem4a  18794  ovollb2  18848  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliun2  18865  ioombl1lem4  18918  uniioombllem1  18936  uniioombllem2  18938  uniioombllem6  18943  itg2monolem1  19105  itg2mono  19108  itg2cnlem1  19116  xrlimcnp  20263  efrlim  20264  ex-br  20818  vcoprne  21135  rge0scvg  23373  limvinlv  25559  topjoin  26314  aomclem1  27151  dfac21  27164  frlmlbs  27249  pclfinN  30089
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator