Theorem syl5eqel 2124

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

Hypotheses

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

Assertion

Ref	Expression
syl5eqel	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl5eqel

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

Syntax hints:   → wi 4   = wceq 1243   ∈ wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  syl5eqelr  2125  csbexga  3885  otexg  3967  tpexg  4179  dmresexg  4634  f1oabexg  5138  funfvex  5192  riotaexg  5472  riotaprop  5491  fnovex  5538  ovexg  5539  fovrn  5643  fnovrn  5648  cofunexg  5738  cofunex2g  5739  abrexex2g  5747  xpexgALT  5760  mpt2fvex  5829  tfrex  5954  frec0g  5983  ecexg  6110  qsexg  6162  diffifi  6351  addvalex  6920  negcl  7211  intqfrac2  9161  intfracq  9162  frecuzrdgrrn  9194  climmpt  9821  ialgcvg  9887  ialgcvga  9890  ialgfx  9891  bj-snexg  10032