Theorem eqeltrdi 2325

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

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

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 2216

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

This theorem is referenced by:  eqeltrrdi  2326  snexprc  4304  onsucelsucexmidlem  4656  dcextest  4708  nnpredcl  4750  ovprc  6094  nnmcl  6727  xpsnen  7085  pw1fin  7183  xpfi  7205  mapfi  7227  snexxph  7233  0fsupp  7264  ctssdclemn0  7414  nninfisollemne  7435  nninfisol  7437  exmidonfinlem  7509  pw1on  7549  indpi  7673  nq0m0r  7787  genpelxp  7842  un0mulcl  9547  znegcl  9625  zeo  9701  eqreznegel  9964  xnegcl  10184  modqid0  10736  q2txmodxeq0  10770  ser0  10919  expcllem  10936  m1expcl2  10947  nn0ltexp2  11096  bcval  11136  bccl  11154  hashinfom  11166  lswex  11301  pfxclz  11396  pfxwrdsymbg  11407  cats1un  11438  cats1fvn  11481  cats1fvnd  11482  resqrexlemlo  11723  iserge0  12053  sumrbdclem  12088  fsum3cvg  12089  summodclem3  12091  summodclem2a  12092  fisumss  12103  binom  12195  bcxmas  12200  prodf1  12253  prodrbdclem  12282  fproddccvg  12283  prodmodclem2a  12287  fprodntrivap  12295  prodssdc  12300  fprodssdc  12301  gcdval  12680  gcdcl  12687  lcmcl  12794  pcxnn0cl  13033  pcxcl  13034  pcmptcl  13065  infpnlem2  13083  zgz  13096  4sqlem19  13132  ballotfilemrval  13205  znf1o  14925  ssblps  15416  ssbl  15417  xmeter  15427  blssioo  15544  elply  15725  plycj  15752  1sgmprm  15988  lgslem4  16002  lgsne0  16037  2sqlem9  16123  2sqlem10  16124  uhgr0enedgfi  16357  vtxdgfi0e  16416  eulerpathprum  16601  bj-charfun  16703  012of  16893  2o01f  16894  nninfsellemeqinf  16920  nninffeq  16924  trilpolemclim  16946  iswomni0  16962