Theorem eleqtrdi 2324

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleqtrrdi  2325  prid2g  3776  freccllem  6567  nninfisol  7331  finomni  7338  exmidomniim  7339  ismkvnex  7353  exmidaclem  7422  pw1m  7441  caucvgprprlem2  7929  gt0srpr  7967  eluzel2  9759  fseq1p1m1  10328  fznn0sub2  10362  nn0split  10370  nnsplit  10371  exple1  10856  bcval5  11024  bcpasc  11027  zfz1isolemsplit  11101  seq3coll  11105  ccatrn  11185  swrdccat2  11251  cats1un  11301  pfxccatin12lem3  11312  cats1fvd  11346  clim2ser  11897  clim2ser2  11898  iserex  11899  isermulc2  11900  iserle  11902  iserge0  11903  climub  11904  climserle  11905  serf0  11912  summodclem3  11940  summodclem2a  11941  fsum3  11947  sum0  11948  fsumcl2lem  11958  fsumadd  11966  isumclim3  11983  isumadd  11991  fsump1i  11993  fsummulc2  12008  cvgcmpub  12036  binom1dif  12047  isumshft  12050  isumsplit  12051  isumrpcl  12054  arisum2  12059  trireciplem  12060  geoserap  12067  geolim  12071  geo2lim  12076  cvgratnnlemnexp  12084  cvgratnnlemseq  12086  cvgratgt0  12093  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  clim2prod  12099  clim2divap  12100  prodmodclem3  12135  prodmodclem2a  12136  fprodseq  12143  fprodntrivap  12144  fprodssdc  12150  fprodmul  12151  fprodabs  12176  fprodeq0  12177  efcvgfsum  12227  efcj  12233  effsumlt  12252  mod2eq1n2dvds  12439  bitsfzolem  12514  bitsfzo  12515  bitsfi  12517  bitsinv1lem  12521  bitsinv1  12522  nninfctlemfo  12610  algrp1  12617  phiprmpw  12793  crth  12795  phimullem  12796  prmdiv  12806  pcpremul  12865  pcmpt  12915  pcfac  12922  pockthlem  12928  pockthg  12929  1arith  12939  ennnfonelemp1  13026  nninfdclemp1  13070  relelbasov  13144  gsumwsubmcl  13578  gsumwmhm  13580  mulgnnp1  13716  mulgnn0z  13735  mulgnndir  13737  idomdomd  14290  idomcringd  14291  lspprid2  14425  istps  14755  topontopn  14760  cldrcl  14825  cnrehmeocntop  15333  elplyd  15464  ply1termlem  15465  ply1term  15466  plyaddlem1  15470  plymullem1  15471  plyaddlem  15472  plymullem  15473  plycoeid3  15480  plycolemc  15481  plycj  15484  dvply1  15488  0sgmppw  15716  1sgmprm  15717  lgsval2lem  15738  lgsdir2lem3  15758  lgsdir2lem5  15760  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  gausslemma2dlem3  15791  lgseisenlem1  15798  lgseisenlem4  15801  lgsquadlem2  15806  umgrpredgv  15997  subgruhgredgdm  16120  2omap  16594  nnsf  16607  nninfsellemqall  16617  nninfomnilem  16620  nnnninfex  16624  nninfnfiinf  16625  cvgcmp2nlemabs  16636  trilpolemeq1  16644  nconstwlpolemgt0  16668