Theorem eleqtrdi 2331

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleqtrrdi  2332  prid2g  3816  freccllem  6673  2omap  7318  nninfisol  7473  finomni  7480  exmidomniim  7481  ismkvnex  7495  exmidaclem  7564  pw1m  7583  caucvgprprlem2  8077  gt0srpr  8115  indfdc  9300  eluzel2  9935  fseq1p1m1  10511  fznn0sub2  10545  nn0split  10553  nnsplit  10554  exple1  11045  bcval5  11215  bcpasc  11218  hashf1  11301  zfz1isolemsplit  11304  seq3coll  11308  ccatrn  11391  swrdccat2  11457  cats1un  11507  pfxccatin12lem3  11518  cats1fvd  11552  clim2ser  12119  clim2ser2  12120  iserex  12121  isermulc2  12122  iserle  12124  iserge0  12125  climub  12126  climserle  12127  serf0  12134  summodclem3  12163  summodclem2a  12164  fsum3  12170  sum0  12171  fsumcl2lem  12181  fsumadd  12189  isumclim3  12206  isumadd  12214  fsump1i  12216  fsummulc2  12231  cvgcmpub  12259  binom1dif  12270  isumshft  12273  isumsplit  12274  isumrpcl  12277  arisum2  12282  trireciplem  12283  geoserap  12290  geolim  12294  geo2lim  12299  cvgratnnlemnexp  12307  cvgratnnlemseq  12309  cvgratgt0  12316  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  clim2prod  12322  clim2divap  12323  prodmodclem3  12358  prodmodclem2a  12359  fprodseq  12366  fprodntrivap  12367  fprodssdc  12373  fprodmul  12374  fprodabs  12399  fprodeq0  12400  efcvgfsum  12450  efcj  12456  effsumlt  12475  mod2eq1n2dvds  12662  bitsfzolem  12737  bitsfzo  12738  bitsfi  12740  bitsinv1lem  12744  bitsinv1  12745  nninfctlemfo  12833  algrp1  12840  phiprmpw  13020  crth  13022  phimullem  13023  prmdiv  13033  pcpremul  13092  pcmpt  13142  pcfac  13149  pockthlem  13155  pockthg  13156  1arith  13166  ballotfilem2  13277  ballotfilemfrceq  13321  ennnfonelemp1  13346  nninfdclemp1  13390  relelbasov  13465  gzsumwsubmcl  13850  gzsumwmhm  13852  mulgnnp1  13982  mulgnn0z  14001  mulgnndir  14003  gsump1  14206  idomdomd  14635  idomcringd  14636  lspprid2  14798  istps  15182  topontopn  15187  cldrcl  15252  cnrehmeocntop  15760  elplyd  15891  ply1termlem  15892  ply1term  15893  plyaddlem1  15897  plymullem1  15898  plyaddlem  15899  plymullem  15900  plycoeid3  15907  plycolemc  15908  plycj  15911  dvply1  15915  birthdaylem2  16145  birthdaylem3  16146  ppiprm  16170  ppinprm  16171  0sgmppw  16188  1sgmprm  16189  ppiublem2  16193  bposlem5  16213  lgsval2lem  16227  lgsdir2lem3  16247  lgsdir2lem5  16249  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  gausslemma2dlem3  16280  lgseisenlem1  16287  lgseisenlem4  16290  lgsquadlem2  16295  umgrpredgv  16486  subgruhgredgdm  16609  eupth2lemsfi  16817  depindlem1  16845  nnsf  17146  nninfsellemqall  17156  nninfomnilem  17159  nnnninfex  17163  nninfnfiinf  17164  cvgcmp2nlemabs  17179  trilpolemeq1  17187  nconstwlpolemgt0  17212