Theorem eleqtrdi 2263

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 2249	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleqtrrdi  2264  prid2g  3688  freccllem  6381  nninfisol  7109  finomni  7116  exmidomniim  7117  ismkvnex  7131  exmidaclem  7185  caucvgprprlem2  7672  gt0srpr  7710  eluzel2  9492  fseq1p1m1  10050  fznn0sub2  10084  nn0split  10092  nnsplit  10093  exple1  10532  bcval5  10697  bcpasc  10700  zfz1isolemsplit  10773  seq3coll  10777  clim2ser  11300  clim2ser2  11301  iserex  11302  isermulc2  11303  iserle  11305  iserge0  11306  climub  11307  climserle  11308  serf0  11315  summodclem3  11343  summodclem2a  11344  fsum3  11350  sum0  11351  fsumcl2lem  11361  fsumadd  11369  isumclim3  11386  isumadd  11394  fsump1i  11396  fsummulc2  11411  cvgcmpub  11439  binom1dif  11450  isumshft  11453  isumsplit  11454  isumrpcl  11457  arisum2  11462  trireciplem  11463  geoserap  11470  geolim  11474  geo2lim  11479  cvgratnnlemnexp  11487  cvgratnnlemseq  11489  cvgratgt0  11496  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  clim2prod  11502  clim2divap  11503  prodmodclem3  11538  prodmodclem2a  11539  fprodseq  11546  fprodntrivap  11547  fprodssdc  11553  fprodmul  11554  fprodabs  11579  fprodeq0  11580  efcvgfsum  11630  efcj  11636  effsumlt  11655  mod2eq1n2dvds  11838  algrp1  12000  phiprmpw  12176  crth  12178  phimullem  12179  prmdiv  12189  pcpremul  12247  pcmpt  12295  pcfac  12302  pockthlem  12308  pockthg  12309  1arith  12319  ennnfonelemp1  12361  nninfdclemp1  12405  istps  12824  topontopn  12829  cldrcl  12896  cnrehmeocntop  13387  lgsval2lem  13705  lgsdir2lem3  13725  lgsdir2lem5  13727  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  nnsf  14038  nninfsellemqall  14048  nninfomnilem  14051  cvgcmp2nlemabs  14064  trilpolemeq1  14072  nconstwlpolemgt0  14095