Theorem eleqtrdi 2289

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleqtrrdi  2290  prid2g  3728  freccllem  6464  nninfisol  7203  finomni  7210  exmidomniim  7211  ismkvnex  7225  exmidaclem  7280  caucvgprprlem2  7782  gt0srpr  7820  eluzel2  9611  fseq1p1m1  10174  fznn0sub2  10208  nn0split  10216  nnsplit  10217  exple1  10692  bcval5  10860  bcpasc  10863  zfz1isolemsplit  10935  seq3coll  10939  clim2ser  11507  clim2ser2  11508  iserex  11509  isermulc2  11510  iserle  11512  iserge0  11513  climub  11514  climserle  11515  serf0  11522  summodclem3  11550  summodclem2a  11551  fsum3  11557  sum0  11558  fsumcl2lem  11568  fsumadd  11576  isumclim3  11593  isumadd  11601  fsump1i  11603  fsummulc2  11618  cvgcmpub  11646  binom1dif  11657  isumshft  11660  isumsplit  11661  isumrpcl  11664  arisum2  11669  trireciplem  11670  geoserap  11677  geolim  11681  geo2lim  11686  cvgratnnlemnexp  11694  cvgratnnlemseq  11696  cvgratgt0  11703  mertenslemi1  11705  mertenslem2  11706  mertensabs  11707  clim2prod  11709  clim2divap  11710  prodmodclem3  11745  prodmodclem2a  11746  fprodseq  11753  fprodntrivap  11754  fprodssdc  11760  fprodmul  11761  fprodabs  11786  fprodeq0  11787  efcvgfsum  11837  efcj  11843  effsumlt  11862  mod2eq1n2dvds  12049  bitsfzolem  12124  bitsfzo  12125  bitsfi  12127  bitsinv1lem  12131  bitsinv1  12132  nninfctlemfo  12220  algrp1  12227  phiprmpw  12403  crth  12405  phimullem  12406  prmdiv  12416  pcpremul  12475  pcmpt  12525  pcfac  12532  pockthlem  12538  pockthg  12539  1arith  12549  ennnfonelemp1  12636  nninfdclemp1  12680  relelbasov  12753  gsumwsubmcl  13175  gsumwmhm  13177  mulgnnp1  13307  mulgnn0z  13326  mulgnndir  13328  idomdomd  13880  idomcringd  13881  lspprid2  14015  istps  14315  topontopn  14320  cldrcl  14385  cnrehmeocntop  14893  elplyd  15024  ply1termlem  15025  ply1term  15026  plyaddlem1  15030  plymullem1  15031  plyaddlem  15032  plymullem  15033  plycoeid3  15040  plycolemc  15041  plycj  15044  dvply1  15048  0sgmppw  15276  1sgmprm  15277  lgsval2lem  15298  lgsdir2lem3  15318  lgsdir2lem5  15320  lgsdir  15323  lgsdilem2  15324  lgsdi  15325  lgsne0  15326  gausslemma2dlem3  15351  lgseisenlem1  15358  lgseisenlem4  15361  lgsquadlem2  15366  2omap  15689  nnsf  15699  nninfsellemqall  15709  nninfomnilem  15712  cvgcmp2nlemabs  15726  trilpolemeq1  15734  nconstwlpolemgt0  15758