Theorem eqeltrdi 2323

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

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

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 2214

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

This theorem is referenced by:  eqeltrrdi  2324  snexprc  4299  onsucelsucexmidlem  4651  dcextest  4703  nnpredcl  4745  ovprc  6086  nnmcl  6714  xpsnen  7072  pw1fin  7170  xpfi  7192  mapfi  7214  snexxph  7220  0fsupp  7251  ctssdclemn0  7401  nninfisollemne  7422  nninfisol  7424  exmidonfinlem  7496  pw1on  7536  indpi  7657  nq0m0r  7771  genpelxp  7826  un0mulcl  9530  znegcl  9608  zeo  9683  eqreznegel  9946  xnegcl  10165  modqid0  10712  q2txmodxeq0  10746  ser0  10895  expcllem  10912  m1expcl2  10923  nn0ltexp2  11071  bcval  11111  bccl  11129  hashinfom  11141  lswex  11276  pfxclz  11371  pfxwrdsymbg  11382  cats1un  11413  cats1fvn  11456  cats1fvnd  11457  resqrexlemlo  11698  iserge0  12028  sumrbdclem  12063  fsum3cvg  12064  summodclem3  12066  summodclem2a  12067  fisumss  12078  binom  12170  bcxmas  12175  prodf1  12228  prodrbdclem  12257  fproddccvg  12258  prodmodclem2a  12262  fprodntrivap  12270  prodssdc  12275  fprodssdc  12276  gcdval  12655  gcdcl  12662  lcmcl  12769  pcxnn0cl  13008  pcxcl  13009  pcmptcl  13040  infpnlem2  13058  zgz  13071  4sqlem19  13107  znf1o  14799  ssblps  15290  ssbl  15291  xmeter  15301  blssioo  15418  elply  15599  plycj  15626  1sgmprm  15862  lgslem4  15876  lgsne0  15911  2sqlem9  15997  2sqlem10  15998  uhgr0enedgfi  16231  vtxdgfi0e  16290  eulerpathprum  16475  bj-charfun  16577  012of  16767  2o01f  16768  nninfsellemeqinf  16794  nninffeq  16798  trilpolemclim  16820  iswomni0  16836