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  9597  znegcl  9675  zeo  9751  eqreznegel  10014  xnegcl  10234  modqid0  10787  q2txmodxeq0  10821  ser0  10970  expcllem  10987  m1expcl2  10998  nn0ltexp2  11147  bcval  11187  bccl  11205  hashinfom  11217  lswex  11356  pfxclz  11451  pfxwrdsymbg  11462  cats1un  11493  cats1fvn  11536  cats1fvnd  11537  resqrexlemlo  11779  iserge0  12109  sumrbdclem  12144  fsum3cvg  12145  summodclem3  12147  summodclem2a  12148  fisumss  12159  binom  12251  bcxmas  12256  prodf1  12309  prodrbdclem  12338  fproddccvg  12339  prodmodclem2a  12343  fprodntrivap  12351  prodssdc  12356  fprodssdc  12357  gcdval  12736  gcdcl  12743  lcmcl  12850  pcxnn0cl  13089  pcxcl  13090  pcmptcl  13121  infpnlem2  13139  zgz  13152  4sqlem19  13188  ballotfilemrval  13261  znf1o  14986  ssblps  15526  ssbl  15527  xmeter  15537  blssioo  15654  elply  15835  plycj  15862  1sgmprm  16108  lgslem4  16122  lgsne0  16157  2sqlem9  16243  2sqlem10  16244  uhgr0enedgfi  16477  vtxdgfi0e  16536  eulerpathprum  16721  bj-charfun  16833  012of  17023  2o01f  17024  nninfsellemeqinf  17059  nninffeq  17063  trilpolemclim  17085  iswomni0  17101