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 1398   ∈ 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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  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  3780  freccllem  6611  nninfisol  7392  finomni  7399  exmidomniim  7400  ismkvnex  7414  exmidaclem  7483  pw1m  7502  caucvgprprlem2  7990  gt0srpr  8028  eluzel2  9821  fseq1p1m1  10391  fznn0sub2  10425  nn0split  10433  nnsplit  10434  exple1  10920  bcval5  11088  bcpasc  11091  zfz1isolemsplit  11165  seq3coll  11169  ccatrn  11252  swrdccat2  11318  cats1un  11368  pfxccatin12lem3  11379  cats1fvd  11413  clim2ser  11977  clim2ser2  11978  iserex  11979  isermulc2  11980  iserle  11982  iserge0  11983  climub  11984  climserle  11985  serf0  11992  summodclem3  12021  summodclem2a  12022  fsum3  12028  sum0  12029  fsumcl2lem  12039  fsumadd  12047  isumclim3  12064  isumadd  12072  fsump1i  12074  fsummulc2  12089  cvgcmpub  12117  binom1dif  12128  isumshft  12131  isumsplit  12132  isumrpcl  12135  arisum2  12140  trireciplem  12141  geoserap  12148  geolim  12152  geo2lim  12157  cvgratnnlemnexp  12165  cvgratnnlemseq  12167  cvgratgt0  12174  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  clim2prod  12180  clim2divap  12181  prodmodclem3  12216  prodmodclem2a  12217  fprodseq  12224  fprodntrivap  12225  fprodssdc  12231  fprodmul  12232  fprodabs  12257  fprodeq0  12258  efcvgfsum  12308  efcj  12314  effsumlt  12333  mod2eq1n2dvds  12520  bitsfzolem  12595  bitsfzo  12596  bitsfi  12598  bitsinv1lem  12602  bitsinv1  12603  nninfctlemfo  12691  algrp1  12698  phiprmpw  12874  crth  12876  phimullem  12877  prmdiv  12887  pcpremul  12946  pcmpt  12996  pcfac  13003  pockthlem  13009  pockthg  13010  1arith  13020  ennnfonelemp1  13107  nninfdclemp1  13151  relelbasov  13225  gsumwsubmcl  13659  gsumwmhm  13661  mulgnnp1  13797  mulgnn0z  13816  mulgnndir  13818  idomdomd  14373  idomcringd  14374  lspprid2  14508  istps  14843  topontopn  14848  cldrcl  14913  cnrehmeocntop  15421  elplyd  15552  ply1termlem  15553  ply1term  15554  plyaddlem1  15558  plymullem1  15559  plyaddlem  15560  plymullem  15561  plycoeid3  15568  plycolemc  15569  plycj  15572  dvply1  15576  0sgmppw  15807  1sgmprm  15808  lgsval2lem  15829  lgsdir2lem3  15849  lgsdir2lem5  15851  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  gausslemma2dlem3  15882  lgseisenlem1  15889  lgseisenlem4  15892  lgsquadlem2  15897  umgrpredgv  16088  subgruhgredgdm  16211  eupth2lemsfi  16419  depindlem1  16447  2omap  16715  nnsf  16731  nninfsellemqall  16741  nninfomnilem  16744  nnnninfex  16748  nninfnfiinf  16749  cvgcmp2nlemabs  16764  trilpolemeq1  16772  nconstwlpolemgt0  16797  gfsump1  16815