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 1397   ∈ 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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  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  4276  onsucelsucexmidlem  4627  dcextest  4679  nnpredcl  4721  ovprc  6054  nnmcl  6649  xpsnen  7005  pw1fin  7102  xpfi  7124  snexxph  7149  ctssdclemn0  7309  nninfisollemne  7330  nninfisol  7332  exmidonfinlem  7404  pw1on  7444  indpi  7562  nq0m0r  7676  genpelxp  7731  un0mulcl  9436  znegcl  9510  zeo  9585  eqreznegel  9848  xnegcl  10067  modqid0  10613  q2txmodxeq0  10647  ser0  10796  expcllem  10813  m1expcl2  10824  nn0ltexp2  10972  bcval  11012  bccl  11030  hashinfom  11041  lswex  11169  pfxclz  11264  pfxwrdsymbg  11275  cats1un  11306  cats1fvn  11349  cats1fvnd  11350  resqrexlemlo  11578  iserge0  11908  sumrbdclem  11943  fsum3cvg  11944  summodclem3  11946  summodclem2a  11947  fisumss  11958  binom  12050  bcxmas  12055  prodf1  12108  prodrbdclem  12137  fproddccvg  12138  prodmodclem2a  12142  fprodntrivap  12150  prodssdc  12155  fprodssdc  12156  gcdval  12535  gcdcl  12542  lcmcl  12649  pcxnn0cl  12888  pcxcl  12889  pcmptcl  12920  infpnlem2  12938  zgz  12951  4sqlem19  12987  znf1o  14671  ssblps  15155  ssbl  15156  xmeter  15166  blssioo  15283  elply  15464  plycj  15491  1sgmprm  15724  lgslem4  15738  lgsne0  15773  2sqlem9  15859  2sqlem10  15860  uhgr0enedgfi  16093  vtxdgfi0e  16152  eulerpathprum  16337  bj-charfun  16428  012of  16618  2o01f  16619  nninfsellemeqinf  16644  nninffeq  16648  trilpolemclim  16666  iswomni0  16682