Theorem eleqtrdi 2232

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

Hypotheses

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

Assertion

Ref	Expression
eleqtrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrdi

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eleqtrrdi  2233  prid2g  3628  freccllem  6299  finomni  7012  exmidomniim  7013  ismkvnex  7029  exmidaclem  7064  caucvgprprlem2  7518  gt0srpr  7556  eluzel2  9331  fseq1p1m1  9874  fznn0sub2  9905  nn0split  9913  nnsplit  9914  exple1  10349  bcval5  10509  bcpasc  10512  zfz1isolemsplit  10581  seq3coll  10585  clim2ser  11106  clim2ser2  11107  iserex  11108  isermulc2  11109  iserle  11111  iserge0  11112  climub  11113  climserle  11114  serf0  11121  summodclem3  11149  summodclem2a  11150  fsum3  11156  sum0  11157  fsumcl2lem  11167  fsumadd  11175  isumclim3  11192  isumadd  11200  fsump1i  11202  fsummulc2  11217  cvgcmpub  11245  binom1dif  11256  isumshft  11259  isumsplit  11260  isumrpcl  11263  arisum2  11268  trireciplem  11269  geoserap  11276  geolim  11280  geo2lim  11285  cvgratnnlemnexp  11293  cvgratnnlemseq  11295  cvgratgt0  11302  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  clim2prod  11308  clim2divap  11309  prodmodclem3  11344  prodmodclem2a  11345  efcvgfsum  11373  efcj  11379  effsumlt  11398  mod2eq1n2dvds  11576  algrp1  11727  phiprmpw  11898  crth  11900  phimullem  11901  ennnfonelemp1  11919  istps  12199  topontopn  12204  cldrcl  12271  cnrehmeocntop  12762  nnsf  13199  nninfsellemqall  13211  nninfomnilem  13214  cvgcmp2nlemabs  13227  trilpolemeq1  13233