Theorem eleqtrdi 2324

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eleqtrdi.1	|- ( ph -> A e. B )
eleqtrdi.2	|- B = C

Assertion

Ref	Expression
eleqtrdi	|- ( ph -> A e. C )

Proof of Theorem eleqtrdi

Step	Hyp	Ref	Expression
1		eleqtrdi.1	. 2 |- ( ph -> A e. B )
2		eleqtrdi.2	. . 3 |- B = C
3	2	a1i 9	. 2 |- ( ph -> B = C )
4	1, 3	eleqtrd 2310	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1397   e. 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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  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  3776  freccllem  6568  nninfisol  7332  finomni  7339  exmidomniim  7340  ismkvnex  7354  exmidaclem  7423  pw1m  7442  caucvgprprlem2  7930  gt0srpr  7968  eluzel2  9760  fseq1p1m1  10329  fznn0sub2  10363  nn0split  10371  nnsplit  10372  exple1  10858  bcval5  11026  bcpasc  11029  zfz1isolemsplit  11103  seq3coll  11107  ccatrn  11190  swrdccat2  11256  cats1un  11306  pfxccatin12lem3  11317  cats1fvd  11351  clim2ser  11915  clim2ser2  11916  iserex  11917  isermulc2  11918  iserle  11920  iserge0  11921  climub  11922  climserle  11923  serf0  11930  summodclem3  11959  summodclem2a  11960  fsum3  11966  sum0  11967  fsumcl2lem  11977  fsumadd  11985  isumclim3  12002  isumadd  12010  fsump1i  12012  fsummulc2  12027  cvgcmpub  12055  binom1dif  12066  isumshft  12069  isumsplit  12070  isumrpcl  12073  arisum2  12078  trireciplem  12079  geoserap  12086  geolim  12090  geo2lim  12095  cvgratnnlemnexp  12103  cvgratnnlemseq  12105  cvgratgt0  12112  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  clim2prod  12118  clim2divap  12119  prodmodclem3  12154  prodmodclem2a  12155  fprodseq  12162  fprodntrivap  12163  fprodssdc  12169  fprodmul  12170  fprodabs  12195  fprodeq0  12196  efcvgfsum  12246  efcj  12252  effsumlt  12271  mod2eq1n2dvds  12458  bitsfzolem  12533  bitsfzo  12534  bitsfi  12536  bitsinv1lem  12540  bitsinv1  12541  nninfctlemfo  12629  algrp1  12636  phiprmpw  12812  crth  12814  phimullem  12815  prmdiv  12825  pcpremul  12884  pcmpt  12934  pcfac  12941  pockthlem  12947  pockthg  12948  1arith  12958  ennnfonelemp1  13045  nninfdclemp1  13089  relelbasov  13163  gsumwsubmcl  13597  gsumwmhm  13599  mulgnnp1  13735  mulgnn0z  13754  mulgnndir  13756  idomdomd  14310  idomcringd  14311  lspprid2  14445  istps  14775  topontopn  14780  cldrcl  14845  cnrehmeocntop  15353  elplyd  15484  ply1termlem  15485  ply1term  15486  plyaddlem1  15490  plymullem1  15491  plyaddlem  15492  plymullem  15493  plycoeid3  15500  plycolemc  15501  plycj  15504  dvply1  15508  0sgmppw  15736  1sgmprm  15737  lgsval2lem  15758  lgsdir2lem3  15778  lgsdir2lem5  15780  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  gausslemma2dlem3  15811  lgseisenlem1  15818  lgseisenlem4  15821  lgsquadlem2  15826  umgrpredgv  16017  subgruhgredgdm  16140  eupth2lemsfi  16348  depindlem1  16376  2omap  16645  nnsf  16658  nninfsellemqall  16668  nninfomnilem  16671  nnnninfex  16675  nninfnfiinf  16676  cvgcmp2nlemabs  16687  trilpolemeq1  16695  nconstwlpolemgt0  16720  gfsump1  16738