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  4325  onsucelsucexmidlem  4678  dcextest  4730  nnpredcl  4772  ovprc  6124  nnmcl  6758  xpsnen  7123  pw1fin  7221  xpfi  7243  mapfi  7265  snexxph  7272  0fsupp  7303  ctssdclemn0  7456  nninfisollemne  7477  nninfisol  7479  exmidonfinlem  7551  pw1on  7591  indpi  7715  nq0m0r  7829  genpelxp  7884  un0mulcl  9608  znegcl  9686  zeo  9762  eqreznegel  10030  xnegcl  10251  modqid0  10808  q2txmodxeq0  10842  ser0  10991  expcllem  11008  m1expcl2  11019  nn0ltexp2  11169  bcval  11209  bccl  11227  hashinfom  11239  lswex  11378  pfxclz  11473  pfxwrdsymbg  11484  cats1un  11515  cats1fvn  11558  cats1fvnd  11559  resqrexlemlo  11801  iserge0  12134  sumrbdclem  12169  fsum3cvg  12170  summodclem3  12172  summodclem2a  12173  fisumss  12184  binom  12276  bcxmas  12281  prodf1  12334  prodrbdclem  12363  fproddccvg  12364  prodmodclem2a  12368  fprodntrivap  12376  prodssdc  12381  fprodssdc  12382  gcdval  12761  gcdcl  12768  lcmcl  12875  pcxnn0cl  13118  pcxcl  13119  pcmptcl  13150  infpnlem2  13168  zgz  13181  4sqlem19  13217  ballotfilemrval  13319  gsum2d2fi  14274  znf1o  15095  ssblps  15651  ssbl  15652  xmeter  15662  blssioo  15779  elply  15960  plycj  15987  1sgmprm  16288  lgslem4  16327  lgsne0  16362  2sqlem9  16448  2sqlem10  16449  uhgr0enedgfi  16682  vtxdgfi0e  16741  eulerpathprum  16926  bj-charfun  17038  012of  17228  2o01f  17229  idjudju  17252  nninfsellemeqinf  17265  nninffeq  17269  trilpolemclim  17292  iswomni0  17308