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  6678  2omap  7324  nninfisol  7479  finomni  7486  exmidomniim  7487  ismkvnex  7501  exmidaclem  7570  pw1m  7589  caucvgprprlem2  8083  gt0srpr  8121  indfdc  9307  eluzel2  9941  fseq1p1m1  10517  fznn0sub2  10551  nn0split  10559  nnsplit  10560  exple1  11052  bcval5  11222  bcpasc  11225  hashf1  11308  zfz1isolemsplit  11311  seq3coll  11315  ccatrn  11398  swrdccat2  11464  cats1un  11514  pfxccatin12lem3  11525  cats1fvd  11559  clim2ser  12127  clim2ser2  12128  iserex  12129  isermulc2  12130  iserle  12132  iserge0  12133  climub  12134  climserle  12135  serf0  12142  summodclem3  12171  summodclem2a  12172  fsum3  12178  sum0  12179  fsumcl2lem  12189  fsumadd  12197  isumclim3  12214  isumadd  12222  fsump1i  12224  fsummulc2  12239  cvgcmpub  12267  binom1dif  12278  isumshft  12281  isumsplit  12282  isumrpcl  12285  arisum2  12290  trireciplem  12291  geoserap  12298  geolim  12302  geo2lim  12307  cvgratnnlemnexp  12315  cvgratnnlemseq  12317  cvgratgt0  12324  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  clim2prod  12330  clim2divap  12331  prodmodclem3  12366  prodmodclem2a  12367  fprodseq  12374  fprodntrivap  12375  fprodssdc  12381  fprodmul  12382  fprodabs  12407  fprodeq0  12408  efcvgfsum  12458  efcj  12464  effsumlt  12483  mod2eq1n2dvds  12670  bitsfzolem  12745  bitsfzo  12746  bitsfi  12748  bitsinv1lem  12752  bitsinv1  12753  nninfctlemfo  12841  algrp1  12848  phiprmpw  13028  crth  13030  phimullem  13031  prmdiv  13041  pcpremul  13100  pcmpt  13150  pcfac  13157  pockthlem  13163  pockthg  13164  1arith  13174  ballotfilem2  13285  ballotfilemfrceq  13329  ennnfonelemp1  13354  nninfdclemp1  13398  relelbasov  13473  gzsumwsubmcl  13859  gzsumwmhm  13861  mulgnnp1  13991  mulgnn0z  14010  mulgnndir  14012  gsump1  14246  idomdomd  14694  idomcringd  14695  lspprid2  14857  istps  15275  topontopn  15280  cldrcl  15345  cnrehmeocntop  15853  elplyd  15984  ply1termlem  15985  ply1term  15986  plyaddlem1  15990  plymullem1  15991  plyaddlem  15992  plymullem  15993  plycoeid3  16000  plycolemc  16001  plycj  16004  dvply1  16008  birthdaylem2  16243  birthdaylem3  16244  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  0sgmppw  16304  1sgmprm  16305  ppiublem2  16309  chtublem  16312  bposlem5  16332  lgsval2lem  16351  lgsdir2lem3  16371  lgsdir2lem5  16373  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  gausslemma2dlem3  16404  lgseisenlem1  16411  lgseisenlem4  16414  lgsquadlem2  16419  umgrpredgv  16610  subgruhgredgdm  16733  eupth2lemsfi  16941  depindlem1  16969  nnsf  17271  nninfsellemqall  17281  nninfomnilem  17284  nnnninfex  17288  nninfnfiinf  17289  cvgcmp2nlemabs  17304  trilpolemeq1  17313  nconstwlpolemgt0  17338