Theorem eqeltrdi 2284

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

Hypotheses

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

Assertion

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

Proof of Theorem eqeltrdi

Step	Hyp	Ref	Expression
1		eqeltrdi.1	. 2 |- ( ph -> A = B )
2		eqeltrdi.2	. . 3 |- B e. C
3	2	a1i 9	. 2 |- ( ph -> B e. C )
4	1, 3	eqeltrd 2270	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:  eqeltrrdi  2285  snexprc  4215  onsucelsucexmidlem  4561  dcextest  4613  nnpredcl  4655  ovprc  5953  nnmcl  6534  xpsnen  6875  pw1fin  6966  xpfi  6986  snexxph  7009  ctssdclemn0  7169  nninfisollemne  7190  nninfisol  7192  exmidonfinlem  7253  pw1on  7286  indpi  7402  nq0m0r  7516  genpelxp  7571  un0mulcl  9274  znegcl  9348  zeo  9422  eqreznegel  9679  xnegcl  9898  modqid0  10421  q2txmodxeq0  10455  ser0  10604  expcllem  10621  m1expcl2  10632  nn0ltexp2  10780  bcval  10820  bccl  10838  hashinfom  10849  resqrexlemlo  11157  iserge0  11486  sumrbdclem  11520  fsum3cvg  11521  summodclem3  11523  summodclem2a  11524  fisumss  11535  binom  11627  bcxmas  11632  prodf1  11685  prodrbdclem  11714  fproddccvg  11715  prodmodclem2a  11719  fprodntrivap  11727  prodssdc  11732  fprodssdc  11733  gcdval  12096  gcdcl  12103  lcmcl  12210  pcxnn0cl  12448  pcxcl  12449  pcmptcl  12480  infpnlem2  12498  zgz  12511  4sqlem19  12547  znf1o  14139  ssblps  14593  ssbl  14594  xmeter  14604  blssioo  14713  elply  14880  lgslem4  15119  lgsne0  15154  2sqlem9  15211  2sqlem10  15212  bj-charfun  15299  012of  15486  2o01f  15487  nninfsellemeqinf  15506  nninffeq  15510  trilpolemclim  15526  iswomni0  15541