Theorem eqeltrdi 2320

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrrdi  2321  snexprc  4270  onsucelsucexmidlem  4621  dcextest  4673  nnpredcl  4715  ovprc  6043  nnmcl  6635  xpsnen  6988  pw1fin  7083  xpfi  7105  snexxph  7128  ctssdclemn0  7288  nninfisollemne  7309  nninfisol  7311  exmidonfinlem  7382  pw1on  7422  indpi  7540  nq0m0r  7654  genpelxp  7709  un0mulcl  9414  znegcl  9488  zeo  9563  eqreznegel  9821  xnegcl  10040  modqid0  10584  q2txmodxeq0  10618  ser0  10767  expcllem  10784  m1expcl2  10795  nn0ltexp2  10943  bcval  10983  bccl  11001  hashinfom  11012  lswex  11136  pfxclz  11226  pfxwrdsymbg  11237  cats1un  11268  cats1fvn  11311  cats1fvnd  11312  resqrexlemlo  11539  iserge0  11869  sumrbdclem  11903  fsum3cvg  11904  summodclem3  11906  summodclem2a  11907  fisumss  11918  binom  12010  bcxmas  12015  prodf1  12068  prodrbdclem  12097  fproddccvg  12098  prodmodclem2a  12102  fprodntrivap  12110  prodssdc  12115  fprodssdc  12116  gcdval  12495  gcdcl  12502  lcmcl  12609  pcxnn0cl  12848  pcxcl  12849  pcmptcl  12880  infpnlem2  12898  zgz  12911  4sqlem19  12947  znf1o  14630  ssblps  15114  ssbl  15115  xmeter  15125  blssioo  15242  elply  15423  plycj  15450  1sgmprm  15683  lgslem4  15697  lgsne0  15732  2sqlem9  15818  2sqlem10  15819  vtxdgfi0e  16054  bj-charfun  16225  012of  16416  2o01f  16417  nninfsellemeqinf  16442  nninffeq  16446  trilpolemclim  16464  iswomni0  16479