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  4219  onsucelsucexmidlem  4565  dcextest  4617  nnpredcl  4659  ovprc  5957  nnmcl  6539  xpsnen  6880  pw1fin  6971  xpfi  6993  snexxph  7016  ctssdclemn0  7176  nninfisollemne  7197  nninfisol  7199  exmidonfinlem  7260  pw1on  7293  indpi  7409  nq0m0r  7523  genpelxp  7578  un0mulcl  9283  znegcl  9357  zeo  9431  eqreznegel  9688  xnegcl  9907  modqid0  10442  q2txmodxeq0  10476  ser0  10625  expcllem  10642  m1expcl2  10653  nn0ltexp2  10801  bcval  10841  bccl  10859  hashinfom  10870  resqrexlemlo  11178  iserge0  11508  sumrbdclem  11542  fsum3cvg  11543  summodclem3  11545  summodclem2a  11546  fisumss  11557  binom  11649  bcxmas  11654  prodf1  11707  prodrbdclem  11736  fproddccvg  11737  prodmodclem2a  11741  fprodntrivap  11749  prodssdc  11754  fprodssdc  11755  gcdval  12126  gcdcl  12133  lcmcl  12240  pcxnn0cl  12479  pcxcl  12480  pcmptcl  12511  infpnlem2  12529  zgz  12542  4sqlem19  12578  znf1o  14207  ssblps  14661  ssbl  14662  xmeter  14672  blssioo  14789  elply  14970  plycj  14997  1sgmprm  15230  lgslem4  15244  lgsne0  15279  2sqlem9  15365  2sqlem10  15366  bj-charfun  15453  012of  15640  2o01f  15641  nninfsellemeqinf  15660  nninffeq  15664  trilpolemclim  15680  iswomni0  15695