Theorem eleqtrdi 2322

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleqtrrdi  2323  prid2g  3771  freccllem  6554  nninfisol  7311  finomni  7318  exmidomniim  7319  ismkvnex  7333  exmidaclem  7401  pw1m  7420  caucvgprprlem2  7908  gt0srpr  7946  eluzel2  9738  fseq1p1m1  10302  fznn0sub2  10336  nn0split  10344  nnsplit  10345  exple1  10829  bcval5  10997  bcpasc  11000  zfz1isolemsplit  11073  seq3coll  11077  ccatrn  11157  swrdccat2  11219  cats1un  11269  pfxccatin12lem3  11280  cats1fvd  11314  clim2ser  11864  clim2ser2  11865  iserex  11866  isermulc2  11867  iserle  11869  iserge0  11870  climub  11871  climserle  11872  serf0  11879  summodclem3  11907  summodclem2a  11908  fsum3  11914  sum0  11915  fsumcl2lem  11925  fsumadd  11933  isumclim3  11950  isumadd  11958  fsump1i  11960  fsummulc2  11975  cvgcmpub  12003  binom1dif  12014  isumshft  12017  isumsplit  12018  isumrpcl  12021  arisum2  12026  trireciplem  12027  geoserap  12034  geolim  12038  geo2lim  12043  cvgratnnlemnexp  12051  cvgratnnlemseq  12053  cvgratgt0  12060  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  clim2prod  12066  clim2divap  12067  prodmodclem3  12102  prodmodclem2a  12103  fprodseq  12110  fprodntrivap  12111  fprodssdc  12117  fprodmul  12118  fprodabs  12143  fprodeq0  12144  efcvgfsum  12194  efcj  12200  effsumlt  12219  mod2eq1n2dvds  12406  bitsfzolem  12481  bitsfzo  12482  bitsfi  12484  bitsinv1lem  12488  bitsinv1  12489  nninfctlemfo  12577  algrp1  12584  phiprmpw  12760  crth  12762  phimullem  12763  prmdiv  12773  pcpremul  12832  pcmpt  12882  pcfac  12889  pockthlem  12895  pockthg  12896  1arith  12906  ennnfonelemp1  12993  nninfdclemp1  13037  relelbasov  13111  gsumwsubmcl  13545  gsumwmhm  13547  mulgnnp1  13683  mulgnn0z  13702  mulgnndir  13704  idomdomd  14257  idomcringd  14258  lspprid2  14392  istps  14722  topontopn  14727  cldrcl  14792  cnrehmeocntop  15300  elplyd  15431  ply1termlem  15432  ply1term  15433  plyaddlem1  15437  plymullem1  15438  plyaddlem  15439  plymullem  15440  plycoeid3  15447  plycolemc  15448  plycj  15451  dvply1  15455  0sgmppw  15683  1sgmprm  15684  lgsval2lem  15705  lgsdir2lem3  15725  lgsdir2lem5  15727  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  gausslemma2dlem3  15758  lgseisenlem1  15765  lgseisenlem4  15768  lgsquadlem2  15773  umgrpredgv  15961  2omap  16446  nnsf  16459  nninfsellemqall  16469  nninfomnilem  16472  nnnninfex  16476  nninfnfiinf  16477  cvgcmp2nlemabs  16488  trilpolemeq1  16496  nconstwlpolemgt0  16520