Theorem syl6eleq 2187

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

Hypotheses

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

Assertion

Ref	Expression
syl6eleq	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl6eleq

Step	Hyp	Ref	Expression
1		syl6eleq.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		syl6eleq.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2173	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1296   ∈ wcel 1445

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 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088  df-clel 2091

This theorem is referenced by:  syl6eleqr  2188  prid2g  3567  freccllem  6205  finomni  6883  exmidomniim  6884  caucvgprprlem2  7366  gt0srpr  7391  eluzel2  9123  fseq1p1m1  9657  fznn0sub2  9688  nn0split  9696  nnsplit  9697  exple1  10142  bcval5  10302  bcpasc  10305  zfz1isolemsplit  10374  seq3coll  10378  clim2ser  10895  clim2ser2  10896  iserex  10897  isermulc2  10898  iserle  10900  iserge0  10901  climub  10902  climserle  10903  serf0  10910  summodclem3  10938  summodclem2a  10939  fsum3  10945  sum0  10946  fsumcl2lem  10956  fsumadd  10964  isumclim3  10981  isumadd  10989  fsump1i  10991  fsummulc2  11006  cvgcmpub  11034  binom1dif  11045  isumshft  11048  isumsplit  11049  isumrpcl  11052  arisum2  11057  trireciplem  11058  geoserap  11065  geolim  11069  geo2lim  11074  cvgratnnlemnexp  11082  cvgratnnlemseq  11084  cvgratgt0  11091  mertenslemi1  11093  mertenslem2  11094  mertensabs  11095  efcvgfsum  11121  efcj  11127  effsumlt  11146  mod2eq1n2dvds  11321  algrp1  11470  phiprmpw  11640  crth  11642  phimullem  11643  istps  11897  topontopn  11902  cldrcl  11969  nnsf  12604  nninfsellemqall  12616  nninfomnilem  12619