Theorem eleqtrdi 2286

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eleqtrrdi  2287  prid2g  3723  freccllem  6455  nninfisol  7192  finomni  7199  exmidomniim  7200  ismkvnex  7214  exmidaclem  7268  caucvgprprlem2  7770  gt0srpr  7808  eluzel2  9597  fseq1p1m1  10160  fznn0sub2  10194  nn0split  10202  nnsplit  10203  exple1  10666  bcval5  10834  bcpasc  10837  zfz1isolemsplit  10909  seq3coll  10913  clim2ser  11480  clim2ser2  11481  iserex  11482  isermulc2  11483  iserle  11485  iserge0  11486  climub  11487  climserle  11488  serf0  11495  summodclem3  11523  summodclem2a  11524  fsum3  11530  sum0  11531  fsumcl2lem  11541  fsumadd  11549  isumclim3  11566  isumadd  11574  fsump1i  11576  fsummulc2  11591  cvgcmpub  11619  binom1dif  11630  isumshft  11633  isumsplit  11634  isumrpcl  11637  arisum2  11642  trireciplem  11643  geoserap  11650  geolim  11654  geo2lim  11659  cvgratnnlemnexp  11667  cvgratnnlemseq  11669  cvgratgt0  11676  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  clim2prod  11682  clim2divap  11683  prodmodclem3  11718  prodmodclem2a  11719  fprodseq  11726  fprodntrivap  11727  fprodssdc  11733  fprodmul  11734  fprodabs  11759  fprodeq0  11760  efcvgfsum  11810  efcj  11816  effsumlt  11835  mod2eq1n2dvds  12020  nninfctlemfo  12177  algrp1  12184  phiprmpw  12360  crth  12362  phimullem  12363  prmdiv  12373  pcpremul  12431  pcmpt  12481  pcfac  12488  pockthlem  12494  pockthg  12495  1arith  12505  ennnfonelemp1  12563  nninfdclemp1  12607  relelbasov  12680  gsumwsubmcl  13068  gsumwmhm  13070  mulgnnp1  13200  mulgnn0z  13219  mulgnndir  13221  idomdomd  13773  idomcringd  13774  lspprid2  13908  istps  14200  topontopn  14205  cldrcl  14270  cnrehmeocntop  14764  elplyd  14887  ply1termlem  14888  ply1term  14889  plyaddlem1  14893  plymullem1  14894  plyaddlem  14895  plymullem  14896  lgsval2lem  15126  lgsdir2lem3  15146  lgsdir2lem5  15148  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  gausslemma2dlem3  15179  lgseisenlem1  15186  lgseisenlem4  15189  nnsf  15495  nninfsellemqall  15505  nninfomnilem  15508  cvgcmp2nlemabs  15522  trilpolemeq1  15530  nconstwlpolemgt0  15554