Theorem eleqtrdi 2300

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eleqtrrdi  2301  prid2g  3748  freccllem  6511  nninfisol  7261  finomni  7268  exmidomniim  7269  ismkvnex  7283  exmidaclem  7351  pw1m  7370  caucvgprprlem2  7858  gt0srpr  7896  eluzel2  9688  fseq1p1m1  10251  fznn0sub2  10285  nn0split  10293  nnsplit  10294  exple1  10777  bcval5  10945  bcpasc  10948  zfz1isolemsplit  11020  seq3coll  11024  ccatrn  11103  swrdccat2  11162  cats1un  11212  pfxccatin12lem3  11223  clim2ser  11763  clim2ser2  11764  iserex  11765  isermulc2  11766  iserle  11768  iserge0  11769  climub  11770  climserle  11771  serf0  11778  summodclem3  11806  summodclem2a  11807  fsum3  11813  sum0  11814  fsumcl2lem  11824  fsumadd  11832  isumclim3  11849  isumadd  11857  fsump1i  11859  fsummulc2  11874  cvgcmpub  11902  binom1dif  11913  isumshft  11916  isumsplit  11917  isumrpcl  11920  arisum2  11925  trireciplem  11926  geoserap  11933  geolim  11937  geo2lim  11942  cvgratnnlemnexp  11950  cvgratnnlemseq  11952  cvgratgt0  11959  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  clim2prod  11965  clim2divap  11966  prodmodclem3  12001  prodmodclem2a  12002  fprodseq  12009  fprodntrivap  12010  fprodssdc  12016  fprodmul  12017  fprodabs  12042  fprodeq0  12043  efcvgfsum  12093  efcj  12099  effsumlt  12118  mod2eq1n2dvds  12305  bitsfzolem  12380  bitsfzo  12381  bitsfi  12383  bitsinv1lem  12387  bitsinv1  12388  nninfctlemfo  12476  algrp1  12483  phiprmpw  12659  crth  12661  phimullem  12662  prmdiv  12672  pcpremul  12731  pcmpt  12781  pcfac  12788  pockthlem  12794  pockthg  12795  1arith  12805  ennnfonelemp1  12892  nninfdclemp1  12936  relelbasov  13009  gsumwsubmcl  13443  gsumwmhm  13445  mulgnnp1  13581  mulgnn0z  13600  mulgnndir  13602  idomdomd  14154  idomcringd  14155  lspprid2  14289  istps  14619  topontopn  14624  cldrcl  14689  cnrehmeocntop  15197  elplyd  15328  ply1termlem  15329  ply1term  15330  plyaddlem1  15334  plymullem1  15335  plyaddlem  15336  plymullem  15337  plycoeid3  15344  plycolemc  15345  plycj  15348  dvply1  15352  0sgmppw  15580  1sgmprm  15581  lgsval2lem  15602  lgsdir2lem3  15622  lgsdir2lem5  15624  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  gausslemma2dlem3  15655  lgseisenlem1  15662  lgseisenlem4  15665  lgsquadlem2  15670  umgrpredgv  15851  2omap  16132  nnsf  16144  nninfsellemqall  16154  nninfomnilem  16157  nnnninfex  16161  nninfnfiinf  16162  cvgcmp2nlemabs  16173  trilpolemeq1  16181  nconstwlpolemgt0  16205