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  6759  xpsnen  7125  pw1fin  7223  xpfi  7245  mapfi  7267  snexxph  7274  ctssdclemn0  7456  nninfisollemne  7477  nninfisol  7479  exmidonfinlem  7551  pw1on  7591  indpi  7715  nq0m0r  7829  genpelxp  7884  un0mulcl  9608  znegcl  9684  zeo  9761  eqreznegel  10029  xnegcl  10250  modqid0  10807  q2txmodxeq0  10841  ser0  10990  expcllem  11007  m1expcl2  11018  nn0ltexp2  11168  bcval  11208  bccl  11226  hashinfom  11238  lswex  11377  pfxclz  11472  pfxwrdsymbg  11483  cats1un  11514  cats1fvn  11557  cats1fvnd  11558  resqrexlemlo  11800  iserge0  12133  sumrbdclem  12168  fsum3cvg  12169  summodclem3  12171  summodclem2a  12172  fisumss  12183  binom  12275  bcxmas  12280  prodf1  12333  prodrbdclem  12362  fproddccvg  12363  prodmodclem2a  12367  fprodntrivap  12375  prodssdc  12380  fprodssdc  12381  gcdval  12760  gcdcl  12767  lcmcl  12874  pcxnn0cl  13117  pcxcl  13118  pcmptcl  13149  infpnlem2  13167  zgz  13180  4sqlem19  13216  ballotfilemrval  13318  gsum2d2fi  14273  znf1o  15094  ssblps  15668  ssbl  15669  xmeter  15679  blssioo  15796  elply  15977  plycj  16004  1sgmprm  16305  lgslem4  16344  lgsne0  16379  2sqlem9  16465  2sqlem10  16466  uhgr0enedgfi  16699  vtxdgfi0e  16758  eulerpathprum  16943  bj-charfun  17055  012of  17245  2o01f  17246  idjudju  17269  nninfsellemeqinf  17282  nninffeq  17286  trilpolemclim  17309  iswomni0  17325