Theorem syl6eqel 2178

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

Hypotheses

Ref	Expression
syl6eqel.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6eqel.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
syl6eqel	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl6eqel

Step	Hyp	Ref	Expression
1		syl6eqel.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6eqel.2	. . 3 ⊢ 𝐵 ∈ 𝐶
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	1, 3	eqeltrd 2164	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1289   ∈ wcel 1438

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  syl6eqelr  2179  snexprc  4021  onsucelsucexmidlem  4345  dcextest  4396  ovprc  5684  nnmcl  6242  xpsnen  6537  xpfi  6640  snexxph  6659  indpi  6901  nq0m0r  7015  genpelxp  7070  un0mulcl  8707  znegcl  8781  zeo  8851  eqreznegel  9099  xnegcl  9294  modqid0  9757  q2txmodxeq0  9791  iser0  9947  ser0  9949  expcllem  9966  m1expcl2  9977  bcval  10157  bccl  10175  hashinfom  10186  resqrexlemlo  10446  iserge0  10732  isumrblem  10765  fisumcvg  10766  fsum3cvg  10767  isummolem3  10770  isummolem2a  10771  fisumss  10784  binom  10878  bcxmas  10883  gcdval  11229  gcdcl  11236  lcmcl  11332  nnpredcl  11890  nninfsellemeqinf  11908