Theorem eleqtrdi 2250

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

Syntax hints:   → wi 4   = wceq 1335   ∈ wcel 2128

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153

This theorem is referenced by:  eleqtrrdi  2251  prid2g  3664  freccllem  6346  nninfisol  7071  finomni  7078  exmidomniim  7079  ismkvnex  7093  exmidaclem  7138  caucvgprprlem2  7625  gt0srpr  7663  eluzel2  9439  fseq1p1m1  9991  fznn0sub2  10022  nn0split  10030  nnsplit  10031  exple1  10470  bcval5  10632  bcpasc  10635  zfz1isolemsplit  10704  seq3coll  10708  clim2ser  11229  clim2ser2  11230  iserex  11231  isermulc2  11232  iserle  11234  iserge0  11235  climub  11236  climserle  11237  serf0  11244  summodclem3  11272  summodclem2a  11273  fsum3  11279  sum0  11280  fsumcl2lem  11290  fsumadd  11298  isumclim3  11315  isumadd  11323  fsump1i  11325  fsummulc2  11340  cvgcmpub  11368  binom1dif  11379  isumshft  11382  isumsplit  11383  isumrpcl  11386  arisum2  11391  trireciplem  11392  geoserap  11399  geolim  11403  geo2lim  11408  cvgratnnlemnexp  11416  cvgratnnlemseq  11418  cvgratgt0  11425  mertenslemi1  11427  mertenslem2  11428  mertensabs  11429  clim2prod  11431  clim2divap  11432  prodmodclem3  11467  prodmodclem2a  11468  fprodseq  11475  fprodntrivap  11476  fprodssdc  11482  fprodmul  11483  fprodabs  11508  fprodeq0  11509  efcvgfsum  11559  efcj  11565  effsumlt  11584  mod2eq1n2dvds  11764  algrp1  11917  phiprmpw  12089  crth  12091  phimullem  12092  prmdiv  12102  ennnfonelemp1  12122  nninfdclemp1  12168  istps  12417  topontopn  12422  cldrcl  12489  cnrehmeocntop  12980  nnsf  13564  nninfsellemqall  13574  nninfomnilem  13577  cvgcmp2nlemabs  13590  trilpolemeq1  13598  nconstwlpolemgt0  13621