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

Theorem syl5eleqr 2383
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 2301 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2382 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696
This theorem is referenced by:  rabsnt  3717  reusv6OLD  4561  onnev  4786  opabiota  6309  canth  6310  onnseq  6377  tfrlem16  6425  oen0  6600  nnawordex  6651  inf0  7338  cantnflt  7389  cnfcom2  7421  cnfcom3lem  7422  cnfcom3  7423  r1ordg  7466  r1val1  7474  rankr1id  7550  acacni  7782  dfacacn  7783  dfac13  7784  cda1dif  7818  ttukeylem5  8156  ttukeylem6  8157  gchac  8311  gch2  8317  gch3  8318  gchina  8337  swrds1  11489  sadcp1  12662  xpsfrnel2  13483  idfucl  13771  gsumz  14474  gsumval2  14476  frmdmnd  14497  frmd0  14498  efginvrel2  15052  efgcpbl2  15082  pgpfaclem1  15332  lbsexg  15933  dfac14  17328  acufl  17628  minveclem3b  18808  minveclem4a  18810  ovollb2  18864  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliun2  18881  ioombl1lem4  18934  uniioombllem1  18952  uniioombllem2  18954  uniioombllem6  18959  itg2monolem1  19121  itg2mono  19124  itg2cnlem1  19132  xrlimcnp  20279  efrlim  20280  ex-br  20834  vcoprne  21151  rge0scvg  23388  limvinlv  25662  topjoin  26417  aomclem1  27254  dfac21  27267  frlmlbs  27352  usgrcyclnl1  28386  pclfinN  30711
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