Theorem eqeltrdi 2329

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 2315	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eqeltrrdi  2330  snexprc  4318  onsucelsucexmidlem  4671  dcextest  4723  nnpredcl  4765  ovprc  6111  nnmcl  6744  xpsnen  7109  pw1fin  7207  xpfi  7229  mapfi  7251  snexxph  7257  0fsupp  7288  ctssdclemn0  7440  nninfisollemne  7461  nninfisol  7463  exmidonfinlem  7535  pw1on  7575  indpi  7699  nq0m0r  7813  genpelxp  7868  un0mulcl  9576  znegcl  9654  zeo  9730  eqreznegel  9993  xnegcl  10213  modqid0  10765  q2txmodxeq0  10799  ser0  10948  expcllem  10965  m1expcl2  10976  nn0ltexp2  11125  bcval  11165  bccl  11183  hashinfom  11195  lswex  11334  pfxclz  11429  pfxwrdsymbg  11440  cats1un  11471  cats1fvn  11514  cats1fvnd  11515  resqrexlemlo  11757  iserge0  12087  sumrbdclem  12122  fsum3cvg  12123  summodclem3  12125  summodclem2a  12126  fisumss  12137  binom  12229  bcxmas  12234  prodf1  12287  prodrbdclem  12316  fproddccvg  12317  prodmodclem2a  12321  fprodntrivap  12329  prodssdc  12334  fprodssdc  12335  gcdval  12714  gcdcl  12721  lcmcl  12828  pcxnn0cl  13067  pcxcl  13068  pcmptcl  13099  infpnlem2  13117  zgz  13130  4sqlem19  13166  ballotfilemrval  13239  znf1o  14958  ssblps  15449  ssbl  15450  xmeter  15460  blssioo  15577  elply  15758  plycj  15785  1sgmprm  16022  lgslem4  16036  lgsne0  16071  2sqlem9  16157  2sqlem10  16158  uhgr0enedgfi  16391  vtxdgfi0e  16450  eulerpathprum  16635  bj-charfun  16747  012of  16937  2o01f  16938  nninfsellemeqinf  16964  nninffeq  16968  trilpolemclim  16990  iswomni0  17006