Theorem syl5eqel 2165

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 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:  syl5eqelr  2166  csbexga  3906  otexg  3985  tpexg  4197  dmresexg  4652  f1oabexg  5158  funfvex  5212  riotaexg  5492  riotaprop  5511  fnovex  5558  ovexg  5559  fovrn  5663  fnovrn  5668  cofunexg  5758  cofunex2g  5759  abrexex2g  5767  xpexgALT  5780  mpt2fvex  5849  tfrex  5977  frec0g  6006  ecexg  6133  qsexg  6185  diffifi  6378  fnfi  6388  funrnfi  6392  infclti  6436  addvalex  7012  negcl  7308  intqfrac2  9321  intfracq  9322  frecuzrdgrrn  9410  ibcval5  9690  climmpt  10139  ialgcvg  10430  ialgcvga  10433  ialgfx  10434  eucialgcvga  10440  eucialg  10441  bj-snexg  10703