Theorem eqeltrdi 2230

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eqeltrrdi  2231  snexprc  4110  onsucelsucexmidlem  4444  dcextest  4495  nnpredcl  4536  ovprc  5806  nnmcl  6377  xpsnen  6715  xpfi  6818  snexxph  6838  ctssdclemn0  6995  exmidonfinlem  7049  indpi  7153  nq0m0r  7267  genpelxp  7322  un0mulcl  9014  znegcl  9088  zeo  9159  eqreznegel  9409  xnegcl  9618  modqid0  10126  q2txmodxeq0  10160  ser0  10290  expcllem  10307  m1expcl2  10318  bcval  10498  bccl  10516  hashinfom  10527  resqrexlemlo  10788  iserge0  11115  sumrbdclem  11149  fsum3cvg  11150  summodclem3  11152  summodclem2a  11153  fisumss  11164  binom  11256  bcxmas  11261  prodf1  11314  prodrbdclem  11343  fproddccvg  11344  prodmodclem2a  11348  gcdval  11651  gcdcl  11658  lcmcl  11756  ssblps  12597  ssbl  12598  xmeter  12608  blssioo  12717  nninfsellemeqinf  13215  nninffeq  13219  isomninnlem  13228  trilpolemclim  13232