Theorem syl6eleq 1558

Description: A membership and equality inference.

Hypotheses

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

Assertion

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

Proof of Theorem syl6eleq

Step	Hyp	Ref	Expression
1		syl6eleq.1	. 2 |- (ph -> A e. B)
2		syl6eleq.2	. . 3 |- B = C
3	2	a1i 8	. 2 |- (ph -> B = C)
4	1, 3	eleqtrd 1550	1 |- (ph -> A e. C)

Syntax hints:   -> wi 3   = wceq 956   e. wcel 958

This theorem is referenced by:  syl6eleqr 1559  ndmfvrcl 3746  tz7.48-1 3956  r1rankid 4694  rankelun 4707  rankelpr 4708  rankelop 4709  alephgeom 4882  icoshftf1oi 6409  eluz2t 6421  binomlem1 7066  binomlem4 7069  binomlem5 7070  fsum0diaglem2 7257  fsum0diag3 7260  efaddlem6 7343  cnpco 7769  ghgrpilem1 8133  ghgrpilem3 8135  ghgrpilem4 8136  pjoc1 9264  shmods 9362  5oalem1 9599  mayete3 9673  adjt 9857  nmcopexlem4 9954  nmcfnexlem4 9983  bra11 10041

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain