Theorem syl6eleqr 1551

Description: A membership and equality inference.

Hypotheses

Ref	Expression
syl6eleqr.1	|- (ph -> A e. B)
syl6eleqr.2	|- C = B

Assertion

Ref	Expression
syl6eleqr	|- (ph -> A e. C)

Proof of Theorem syl6eleqr

Step	Hyp	Ref	Expression
1		syl6eleqr.1	. 2 |- (ph -> A e. B)
2		syl6eleqr.2	. . 3 |- C = B
3	2	eqcomi 1471	. 2 |- B = C
4	1, 3	syl6eleq 1550	1 |- (ph -> A e. C)

Syntax hints:   -> wi 3   = wceq 953   e. wcel 955

This theorem is referenced by:  tpi1 2446  tpi2 2447  tpi3 2448  brelrn 3332  tfrlem11 3906  unielxp 4091  ecopqsi 4277  eceqopreq 4297  th3qlem1 4298  sbthlem2 4428  rankelpr 4680  cardlim 4823  alephfp 4872  enqeceq 5019  addclpq 5030  mulclpq 5032  enreceq 5149  addclsr 5164  mulclsr 5165  axaddopr 5237  axmulopr 5238  cvg1 6858  unbenlem 7447  cnmetdval 7841  lmconst 7872  nmcn2 8275  resslogrn 8675  hmopidmch 9990

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465

Copyright terms: Public domain