Theorem syl5eqel 2186

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

Syntax hints:   → wi 4   = wceq 1299   ∈ wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096

This theorem is referenced by:  syl5eqelr  2187  csbexga  3996  otexg  4090  tpexg  4303  dmresexg  4778  f1oabexg  5313  funfvex  5370  riotaexg  5666  riotaprop  5685  fnovex  5736  ovexg  5737  fovrn  5845  fnovrn  5850  cofunexg  5940  cofunex2g  5941  abrexex2g  5949  xpexgALT  5962  mpofvex  6031  tfrex  6195  frec0g  6224  freccllem  6229  ecexg  6363  qsexg  6415  pmex  6477  elixpsn  6559  diffifi  6717  unfidisj  6739  prfidisj  6744  tpfidisj  6745  ssfirab  6750  ssfidc  6751  fnfi  6753  funrnfi  6758  iunfidisj  6762  infclti  6825  djuex  6843  ctssdclemr  6911  addvalex  7531  negcl  7833  intqfrac2  9933  intfracq  9934  frec2uzzd  10014  frecuzrdgrrn  10022  iseqf1olemqpcl  10110  seq3f1olemqsum  10114  bcval5  10350  xrmaxiflemval  10858  climmpt  10908  reccn2ap  10921  zsumdc  10992  fsumzcl2  11013  fsump1i  11041  fsumabs  11073  hash2iun1dif1  11088  mertenslemi1  11143  algrf  11519  algcvg  11522  algcvga  11525  algfx  11526  eucalgcvga  11532  eucalg  11533  crth  11692  phimullem  11693  ennnfonelemj0  11706  ennnfonelemom  11713  ressid  11802  1strbas  11840  2strbasg  11842  2stropg  11843  restid  11913  topnvalg  11914  topnidg  11915  topopn  11957  topcld  12060  uncld  12064  iuncld  12066  unicld  12067  tgrest  12120  restin  12127  cnco  12171  cnrest  12185  cnptoprest2  12190  lmss  12196  txbasval  12217  txcn  12225  cnmpt12f  12236  blres  12362  metrest  12434  qtopbasss  12443  tgqioo  12466  cncfmet  12492  cdivcncfap  12499  cnplimcim  12516  limccnpcntop  12520  dvfvalap  12523  bj-snexg  12691  trilpolemcl  12814