Theorem eqeltrdi 2287

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eqeltrrdi  2288  snexprc  4220  onsucelsucexmidlem  4566  dcextest  4618  nnpredcl  4660  ovprc  5961  nnmcl  6548  xpsnen  6889  pw1fin  6980  xpfi  7002  snexxph  7025  ctssdclemn0  7185  nninfisollemne  7206  nninfisol  7208  exmidonfinlem  7274  pw1on  7311  indpi  7428  nq0m0r  7542  genpelxp  7597  un0mulcl  9302  znegcl  9376  zeo  9450  eqreznegel  9707  xnegcl  9926  modqid0  10461  q2txmodxeq0  10495  ser0  10644  expcllem  10661  m1expcl2  10672  nn0ltexp2  10820  bcval  10860  bccl  10878  hashinfom  10889  resqrexlemlo  11197  iserge0  11527  sumrbdclem  11561  fsum3cvg  11562  summodclem3  11564  summodclem2a  11565  fisumss  11576  binom  11668  bcxmas  11673  prodf1  11726  prodrbdclem  11755  fproddccvg  11756  prodmodclem2a  11760  fprodntrivap  11768  prodssdc  11773  fprodssdc  11774  gcdval  12153  gcdcl  12160  lcmcl  12267  pcxnn0cl  12506  pcxcl  12507  pcmptcl  12538  infpnlem2  12556  zgz  12569  4sqlem19  12605  znf1o  14285  ssblps  14769  ssbl  14770  xmeter  14780  blssioo  14897  elply  15078  plycj  15105  1sgmprm  15338  lgslem4  15352  lgsne0  15387  2sqlem9  15473  2sqlem10  15474  bj-charfun  15561  012of  15748  2o01f  15749  nninfsellemeqinf  15771  nninffeq  15775  trilpolemclim  15793  iswomni0  15808