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  7272  pw1on  7309  indpi  7426  nq0m0r  7540  genpelxp  7595  un0mulcl  9300  znegcl  9374  zeo  9448  eqreznegel  9705  xnegcl  9924  modqid0  10459  q2txmodxeq0  10493  ser0  10642  expcllem  10659  m1expcl2  10670  nn0ltexp2  10818  bcval  10858  bccl  10876  hashinfom  10887  resqrexlemlo  11195  iserge0  11525  sumrbdclem  11559  fsum3cvg  11560  summodclem3  11562  summodclem2a  11563  fisumss  11574  binom  11666  bcxmas  11671  prodf1  11724  prodrbdclem  11753  fproddccvg  11754  prodmodclem2a  11758  fprodntrivap  11766  prodssdc  11771  fprodssdc  11772  gcdval  12151  gcdcl  12158  lcmcl  12265  pcxnn0cl  12504  pcxcl  12505  pcmptcl  12536  infpnlem2  12554  zgz  12567  4sqlem19  12603  znf1o  14283  ssblps  14745  ssbl  14746  xmeter  14756  blssioo  14873  elply  15054  plycj  15081  1sgmprm  15314  lgslem4  15328  lgsne0  15363  2sqlem9  15449  2sqlem10  15450  bj-charfun  15537  012of  15724  2o01f  15725  nninfsellemeqinf  15747  nninffeq  15751  trilpolemclim  15767  iswomni0  15782