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  7319  nninfisol  7474  finomni  7481  exmidomniim  7482  ismkvnex  7496  exmidaclem  7565  pw1m  7584  caucvgprprlem2  8078  gt0srpr  8116  indfdc  9301  eluzel2  9936  fseq1p1m1  10512  fznn0sub2  10546  nn0split  10554  nnsplit  10555  exple1  11047  bcval5  11217  bcpasc  11220  hashf1  11303  zfz1isolemsplit  11306  seq3coll  11310  ccatrn  11393  swrdccat2  11459  cats1un  11509  pfxccatin12lem3  11520  cats1fvd  11554  clim2ser  12122  clim2ser2  12123  iserex  12124  isermulc2  12125  iserle  12127  iserge0  12128  climub  12129  climserle  12130  serf0  12137  summodclem3  12166  summodclem2a  12167  fsum3  12173  sum0  12174  fsumcl2lem  12184  fsumadd  12192  isumclim3  12209  isumadd  12217  fsump1i  12219  fsummulc2  12234  cvgcmpub  12262  binom1dif  12273  isumshft  12276  isumsplit  12277  isumrpcl  12280  arisum2  12285  trireciplem  12286  geoserap  12293  geolim  12297  geo2lim  12302  cvgratnnlemnexp  12310  cvgratnnlemseq  12312  cvgratgt0  12319  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  clim2prod  12325  clim2divap  12326  prodmodclem3  12361  prodmodclem2a  12362  fprodseq  12369  fprodntrivap  12370  fprodssdc  12376  fprodmul  12377  fprodabs  12402  fprodeq0  12403  efcvgfsum  12453  efcj  12459  effsumlt  12478  mod2eq1n2dvds  12665  bitsfzolem  12740  bitsfzo  12741  bitsfi  12743  bitsinv1lem  12747  bitsinv1  12748  nninfctlemfo  12836  algrp1  12843  phiprmpw  13023  crth  13025  phimullem  13026  prmdiv  13036  pcpremul  13095  pcmpt  13145  pcfac  13152  pockthlem  13158  pockthg  13159  1arith  13169  ballotfilem2  13280  ballotfilemfrceq  13324  ennnfonelemp1  13349  nninfdclemp1  13393  relelbasov  13468  gzsumwsubmcl  13854  gzsumwmhm  13856  mulgnnp1  13986  mulgnn0z  14005  mulgnndir  14007  gsump1  14241  idomdomd  14670  idomcringd  14671  lspprid2  14833  istps  15224  topontopn  15229  cldrcl  15294  cnrehmeocntop  15802  elplyd  15933  ply1termlem  15934  ply1term  15935  plyaddlem1  15939  plymullem1  15940  plyaddlem  15941  plymullem  15942  plycoeid3  15949  plycolemc  15950  plycj  15953  dvply1  15957  birthdaylem2  16187  birthdaylem3  16188  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  0sgmppw  16248  1sgmprm  16249  ppiublem2  16253  chtublem  16256  bposlem5  16276  lgsval2lem  16295  lgsdir2lem3  16315  lgsdir2lem5  16317  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  gausslemma2dlem3  16348  lgseisenlem1  16355  lgseisenlem4  16358  lgsquadlem2  16363  umgrpredgv  16554  subgruhgredgdm  16677  eupth2lemsfi  16885  depindlem1  16913  nnsf  17214  nninfsellemqall  17224  nninfomnilem  17227  nnnninfex  17231  nninfnfiinf  17232  cvgcmp2nlemabs  17247  trilpolemeq1  17256  nconstwlpolemgt0  17281