Theorem syl6eqel 2169

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 2155	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1284   ∈ wcel 1433

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  syl6eqelr  2170  snexprc  3958  onsucelsucexmidlem  4272  ovprc  5560  nnmcl  6083  xpsnen  6318  indpi  6532  nq0m0r  6646  genpelxp  6701  un0mulcl  8322  znegcl  8382  zeo  8452  eqreznegel  8699  xnegcl  8899  modqid0  9352  q2txmodxeq0  9386  iser0  9471  expival  9478  expcllem  9487  m1expcl2  9498  bcval  9676  bccl  9694  resqrexlemlo  9899  iserige0  10181  gcdval  10351  gcdcl  10358  lcmcl  10454