Theorem syl5eqel 2437

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

Hypotheses

Ref	Expression
syl5eqel.1	⊢ A = B
syl5eqel.2	⊢ (φ → B ∈ C)

Assertion

Ref	Expression
syl5eqel	⊢ (φ → A ∈ C)

Proof of Theorem syl5eqel

Step	Hyp	Ref	Expression
1		syl5eqel.1	. . 3 ⊢ A = B
2	1	a1i 10	. 2 ⊢ (φ → A = B)
3		syl5eqel.2	. 2 ⊢ (φ → B ∈ C)
4	2, 3	eqeltrd 2427	1 ⊢ (φ → A ∈ C)

Syntax hints:   → wi 4   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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  3147  complexg  4100  inexg  4101  unexg  4102  difexg  4103  symdifexg  4104  uni1exg  4293  imakexg  4300  pw1exg  4303  cokexg  4310  imagekexg  4312  uniexg  4317  intexg  4320  pwexg  4329  addcexg  4394  nncaddccl  4420  ltfintr  4460  ncfinprop  4475  tfinprop  4490  nnadjoinpw  4522  sfindbl  4531  phiexg  4572  opexg  4588  proj1exg  4592  proj2exg  4593  imaexg  4747  coexg  4750  siexg  4753  cnvexg  5102  rnexg  5105  dmexg  5106  xpexg  5115  resexg  5117  fovrn  5605  fnovrn  5608  txpexg  5785  fixexg  5789  ins2exg  5796  ins3exg  5797  imageexg  5801  pprodexg  5838  fullfunexg  5860  ecexg  5950  qsexg  5983  pmex  6006  pmvalg  6011  nenpw1pwlem1  6085  tccl  6161  frecexg  6313