Theorem eleqtrdi 2282

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

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

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 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  eleqtrrdi  2283  prid2g  3712  freccllem  6426  nninfisol  7160  finomni  7167  exmidomniim  7168  ismkvnex  7182  exmidaclem  7236  caucvgprprlem2  7738  gt0srpr  7776  eluzel2  9562  fseq1p1m1  10123  fznn0sub2  10157  nn0split  10165  nnsplit  10166  exple1  10606  bcval5  10774  bcpasc  10777  zfz1isolemsplit  10849  seq3coll  10853  clim2ser  11376  clim2ser2  11377  iserex  11378  isermulc2  11379  iserle  11381  iserge0  11382  climub  11383  climserle  11384  serf0  11391  summodclem3  11419  summodclem2a  11420  fsum3  11426  sum0  11427  fsumcl2lem  11437  fsumadd  11445  isumclim3  11462  isumadd  11470  fsump1i  11472  fsummulc2  11487  cvgcmpub  11515  binom1dif  11526  isumshft  11529  isumsplit  11530  isumrpcl  11533  arisum2  11538  trireciplem  11539  geoserap  11546  geolim  11550  geo2lim  11555  cvgratnnlemnexp  11563  cvgratnnlemseq  11565  cvgratgt0  11572  mertenslemi1  11574  mertenslem2  11575  mertensabs  11576  clim2prod  11578  clim2divap  11579  prodmodclem3  11614  prodmodclem2a  11615  fprodseq  11622  fprodntrivap  11623  fprodssdc  11629  fprodmul  11630  fprodabs  11655  fprodeq0  11656  efcvgfsum  11706  efcj  11712  effsumlt  11731  mod2eq1n2dvds  11915  algrp1  12077  phiprmpw  12253  crth  12255  phimullem  12256  prmdiv  12266  pcpremul  12324  pcmpt  12374  pcfac  12381  pockthlem  12387  pockthg  12388  1arith  12398  ennnfonelemp1  12456  nninfdclemp1  12500  mulgnnp1  13067  mulgnn0z  13086  mulgnndir  13088  lspprid2  13725  istps  13984  topontopn  13989  cldrcl  14054  cnrehmeocntop  14545  lgsval2lem  14864  lgsdir2lem3  14884  lgsdir2lem5  14886  lgsdir  14889  lgsdilem2  14890  lgsdi  14891  lgsne0  14892  lgseisenlem1  14903  nnsf  15208  nninfsellemqall  15218  nninfomnilem  15221  cvgcmp2nlemabs  15234  trilpolemeq1  15242  nconstwlpolemgt0  15266