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

Theorem syl5eleqr 2523
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 2441 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2522 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  rabsnt  3881  reusv6OLD  4734  onnev  4958  opabiota  6538  canth  6539  onnseq  6606  tfrlem16  6654  oen0  6829  nnawordex  6880  inf0  7576  cantnflt  7627  cnfcom2  7659  cnfcom3lem  7660  cnfcom3  7661  r1ordg  7704  r1val1  7712  rankr1id  7788  acacni  8020  dfacacn  8021  dfac13  8022  cda1dif  8056  ttukeylem5  8393  ttukeylem6  8394  gchac  8548  gch2  8554  gch3  8555  gchina  8574  swrds1  11787  sadcp1  12967  xpsfrnel2  13790  idfucl  14078  gsumz  14781  gsumval2  14783  frmdmnd  14804  frmd0  14805  efginvrel2  15359  efgcpbl2  15389  pgpfaclem1  15639  lbsexg  16236  dfac14  17650  acufl  17949  cnextfvval  18096  cnextcn  18098  minveclem3b  19329  minveclem4a  19331  ovollb2  19385  ovolunlem1a  19392  ovolunlem1  19393  ovoliunlem1  19398  ovoliun2  19402  ioombl1lem4  19455  uniioombllem1  19473  uniioombllem2  19475  uniioombllem6  19480  itg2monolem1  19642  itg2mono  19645  itg2cnlem1  19653  xrlimcnp  20807  efrlim  20808  cusgrares  21481  usgrcyclnl1  21627  ex-br  21739  vcoprne  22058  rge0scvg  24335  topjoin  26394  aomclem1  27129  dfac21  27141  frlmlbs  27226  pclfinN  30697
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator