Theorem eqeltrdi 2329

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eqeltrrdi  2330  snexprc  4323  onsucelsucexmidlem  4676  dcextest  4728  nnpredcl  4770  ovprc  6121  nnmcl  6754  xpsnen  7119  pw1fin  7217  xpfi  7239  mapfi  7261  snexxph  7267  0fsupp  7298  ctssdclemn0  7450  nninfisollemne  7471  nninfisol  7473  exmidonfinlem  7545  pw1on  7585  indpi  7709  nq0m0r  7823  genpelxp  7878  un0mulcl  9601  znegcl  9679  zeo  9755  eqreznegel  10023  xnegcl  10244  modqid0  10800  q2txmodxeq0  10834  ser0  10983  expcllem  11000  m1expcl2  11011  nn0ltexp2  11161  bcval  11201  bccl  11219  hashinfom  11231  lswex  11370  pfxclz  11465  pfxwrdsymbg  11476  cats1un  11507  cats1fvn  11550  cats1fvnd  11551  resqrexlemlo  11793  iserge0  12125  sumrbdclem  12160  fsum3cvg  12161  summodclem3  12163  summodclem2a  12164  fisumss  12175  binom  12267  bcxmas  12272  prodf1  12325  prodrbdclem  12354  fproddccvg  12355  prodmodclem2a  12359  fprodntrivap  12367  prodssdc  12372  fprodssdc  12373  gcdval  12752  gcdcl  12759  lcmcl  12866  pcxnn0cl  13109  pcxcl  13110  pcmptcl  13141  infpnlem2  13159  zgz  13172  4sqlem19  13208  ballotfilemrval  13310  znf1o  15035  ssblps  15575  ssbl  15576  xmeter  15586  blssioo  15703  elply  15884  plycj  15911  1sgmprm  16189  lgslem4  16220  lgsne0  16255  2sqlem9  16341  2sqlem10  16342  uhgr0enedgfi  16575  vtxdgfi0e  16634  eulerpathprum  16819  bj-charfun  16931  012of  17121  2o01f  17122  nninfsellemeqinf  17157  nninffeq  17161  trilpolemclim  17183  iswomni0  17199