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  6568  nninfisol  7332  finomni  7339  exmidomniim  7340  ismkvnex  7354  exmidaclem  7423  pw1m  7442  caucvgprprlem2  7930  gt0srpr  7968  eluzel2  9760  fseq1p1m1  10329  fznn0sub2  10363  nn0split  10371  nnsplit  10372  exple1  10857  bcval5  11025  bcpasc  11028  zfz1isolemsplit  11102  seq3coll  11106  ccatrn  11186  swrdccat2  11252  cats1un  11302  pfxccatin12lem3  11313  cats1fvd  11347  clim2ser  11898  clim2ser2  11899  iserex  11900  isermulc2  11901  iserle  11903  iserge0  11904  climub  11905  climserle  11906  serf0  11913  summodclem3  11942  summodclem2a  11943  fsum3  11949  sum0  11950  fsumcl2lem  11960  fsumadd  11968  isumclim3  11985  isumadd  11993  fsump1i  11995  fsummulc2  12010  cvgcmpub  12038  binom1dif  12049  isumshft  12052  isumsplit  12053  isumrpcl  12056  arisum2  12061  trireciplem  12062  geoserap  12069  geolim  12073  geo2lim  12078  cvgratnnlemnexp  12086  cvgratnnlemseq  12088  cvgratgt0  12095  mertenslemi1  12097  mertenslem2  12098  mertensabs  12099  clim2prod  12101  clim2divap  12102  prodmodclem3  12137  prodmodclem2a  12138  fprodseq  12145  fprodntrivap  12146  fprodssdc  12152  fprodmul  12153  fprodabs  12178  fprodeq0  12179  efcvgfsum  12229  efcj  12235  effsumlt  12254  mod2eq1n2dvds  12441  bitsfzolem  12516  bitsfzo  12517  bitsfi  12519  bitsinv1lem  12523  bitsinv1  12524  nninfctlemfo  12612  algrp1  12619  phiprmpw  12795  crth  12797  phimullem  12798  prmdiv  12808  pcpremul  12867  pcmpt  12917  pcfac  12924  pockthlem  12930  pockthg  12931  1arith  12941  ennnfonelemp1  13028  nninfdclemp1  13072  relelbasov  13146  gsumwsubmcl  13580  gsumwmhm  13582  mulgnnp1  13718  mulgnn0z  13737  mulgnndir  13739  idomdomd  14293  idomcringd  14294  lspprid2  14428  istps  14758  topontopn  14763  cldrcl  14828  cnrehmeocntop  15336  elplyd  15467  ply1termlem  15468  ply1term  15469  plyaddlem1  15473  plymullem1  15474  plyaddlem  15475  plymullem  15476  plycoeid3  15483  plycolemc  15484  plycj  15487  dvply1  15491  0sgmppw  15719  1sgmprm  15720  lgsval2lem  15741  lgsdir2lem3  15761  lgsdir2lem5  15763  lgsdir  15766  lgsdilem2  15767  lgsdi  15768  lgsne0  15769  gausslemma2dlem3  15794  lgseisenlem1  15801  lgseisenlem4  15804  lgsquadlem2  15809  umgrpredgv  16000  subgruhgredgdm  16123  2omap  16597  nnsf  16610  nninfsellemqall  16620  nninfomnilem  16623  nnnninfex  16627  nninfnfiinf  16628  cvgcmp2nlemabs  16639  trilpolemeq1  16647  nconstwlpolemgt0  16671  gfsump1  16689