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  9298  eluzel2  9926  fseq1p1m1  10501  fznn0sub2  10535  nn0split  10543  nnsplit  10544  exple1  11032  bcval5  11201  bcpasc  11204  hashf1  11287  zfz1isolemsplit  11290  seq3coll  11294  ccatrn  11377  swrdccat2  11443  cats1un  11493  pfxccatin12lem3  11504  cats1fvd  11538  clim2ser  12103  clim2ser2  12104  iserex  12105  isermulc2  12106  iserle  12108  iserge0  12109  climub  12110  climserle  12111  serf0  12118  summodclem3  12147  summodclem2a  12148  fsum3  12154  sum0  12155  fsumcl2lem  12165  fsumadd  12173  isumclim3  12190  isumadd  12198  fsump1i  12200  fsummulc2  12215  cvgcmpub  12243  binom1dif  12254  isumshft  12257  isumsplit  12258  isumrpcl  12261  arisum2  12266  trireciplem  12267  geoserap  12274  geolim  12278  geo2lim  12283  cvgratnnlemnexp  12291  cvgratnnlemseq  12293  cvgratgt0  12300  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  clim2prod  12306  clim2divap  12307  prodmodclem3  12342  prodmodclem2a  12343  fprodseq  12350  fprodntrivap  12351  fprodssdc  12357  fprodmul  12358  fprodabs  12383  fprodeq0  12384  efcvgfsum  12434  efcj  12440  effsumlt  12459  mod2eq1n2dvds  12646  bitsfzolem  12721  bitsfzo  12722  bitsfi  12724  bitsinv1lem  12728  bitsinv1  12729  nninfctlemfo  12817  algrp1  12824  phiprmpw  13000  crth  13002  phimullem  13003  prmdiv  13013  pcpremul  13072  pcmpt  13122  pcfac  13129  pockthlem  13135  pockthg  13136  1arith  13146  ballotfilem2  13228  ballotfilemfrceq  13272  ennnfonelemp1  13297  nninfdclemp1  13341  relelbasov  13416  gzsumwsubmcl  13801  gzsumwmhm  13803  mulgnnp1  13933  mulgnn0z  13952  mulgnndir  13954  gsump1  14157  idomdomd  14586  idomcringd  14587  lspprid2  14749  istps  15133  topontopn  15138  cldrcl  15203  cnrehmeocntop  15711  elplyd  15842  ply1termlem  15843  ply1term  15844  plyaddlem1  15848  plymullem1  15849  plyaddlem  15850  plymullem  15851  plycoeid3  15858  plycolemc  15859  plycj  15862  dvply1  15866  birthdaylem2  16088  birthdaylem3  16089  0sgmppw  16107  1sgmprm  16108  lgsval2lem  16129  lgsdir2lem3  16149  lgsdir2lem5  16151  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  gausslemma2dlem3  16182  lgseisenlem1  16189  lgseisenlem4  16192  lgsquadlem2  16197  umgrpredgv  16388  subgruhgredgdm  16511  eupth2lemsfi  16719  depindlem1  16747  nnsf  17048  nninfsellemqall  17058  nninfomnilem  17061  nnnninfex  17065  nninfnfiinf  17066  cvgcmp2nlemabs  17081  trilpolemeq1  17089  nconstwlpolemgt0  17114