Theorem syl5eqel 2437

Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5eqel

Step	Hyp	Ref	Expression
1		syl5eqel.1	. . 3 |- A = B
2	1	a1i 10	. 2 |- (ph -> A = B)
3		syl5eqel.2	. 2 |- (ph -> B e. C)
4	2, 3	eqeltrd 2427	1 |- (ph -> A e. C)

Syntax hints:   -> wi 4   = wceq 1642   e. wcel 1710

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349

This theorem is referenced by:  syl5eqelr  2438  csbexg  3146  complexg  4099  inexg  4100  unexg  4101  difexg  4102  symdifexg  4103  uni1exg  4292  imakexg  4299  pw1exg  4302  cokexg  4309  imagekexg  4311  uniexg  4316  intexg  4319  pwexg  4328  addcexg  4393  nncaddccl  4419  ltfintr  4459  ncfinprop  4474  tfinprop  4489  nnadjoinpw  4521  sfindbl  4530  phiexg  4571  opexg  4587  proj1exg  4591  proj2exg  4592  imaexg  4746  coexg  4749  siexg  4752  cnvexg  5101  rnexg  5104  dmexg  5105  xpexg  5114  resexg  5116  fovrn  5604  fnovrn  5607  txpexg  5784  fixexg  5788  ins2exg  5795  ins3exg  5796  imageexg  5800  pprodexg  5837  fullfunexg  5859  ecexg  5949  qsexg  5982  pmex  6005  pmvalg  6010  nenpw1pwlem1  6084  tccl  6160  frecexg  6312