Theorem eqeltrdi 2322

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

Hypotheses

Ref	Expression
eqeltrdi.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeltrdi.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
eqeltrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrdi

Step	Hyp	Ref	Expression
1		eqeltrdi.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeltrdi.2	. . 3 ⊢ 𝐵 ∈ 𝐶
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	1, 3	eqeltrd 2308	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eqeltrrdi  2323  snexprc  4282  onsucelsucexmidlem  4633  dcextest  4685  nnpredcl  4727  ovprc  6064  nnmcl  6692  xpsnen  7048  pw1fin  7145  xpfi  7167  snexxph  7192  ctssdclemn0  7352  nninfisollemne  7373  nninfisol  7375  exmidonfinlem  7447  pw1on  7487  indpi  7605  nq0m0r  7719  genpelxp  7774  un0mulcl  9478  znegcl  9554  zeo  9629  eqreznegel  9892  xnegcl  10111  modqid0  10658  q2txmodxeq0  10692  ser0  10841  expcllem  10858  m1expcl2  10869  nn0ltexp2  11017  bcval  11057  bccl  11075  hashinfom  11086  lswex  11214  pfxclz  11309  pfxwrdsymbg  11320  cats1un  11351  cats1fvn  11394  cats1fvnd  11395  resqrexlemlo  11636  iserge0  11966  sumrbdclem  12001  fsum3cvg  12002  summodclem3  12004  summodclem2a  12005  fisumss  12016  binom  12108  bcxmas  12113  prodf1  12166  prodrbdclem  12195  fproddccvg  12196  prodmodclem2a  12200  fprodntrivap  12208  prodssdc  12213  fprodssdc  12214  gcdval  12593  gcdcl  12600  lcmcl  12707  pcxnn0cl  12946  pcxcl  12947  pcmptcl  12978  infpnlem2  12996  zgz  13009  4sqlem19  13045  znf1o  14730  ssblps  15219  ssbl  15220  xmeter  15230  blssioo  15347  elply  15528  plycj  15555  1sgmprm  15791  lgslem4  15805  lgsne0  15840  2sqlem9  15926  2sqlem10  15927  uhgr0enedgfi  16160  vtxdgfi0e  16219  eulerpathprum  16404  bj-charfun  16506  012of  16696  2o01f  16697  nninfsellemeqinf  16725  nninffeq  16729  trilpolemclim  16751  iswomni0  16767