Theorem eqeltrdi 2297

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  eqeltrrdi  2298  snexprc  4238  onsucelsucexmidlem  4585  dcextest  4637  nnpredcl  4679  ovprc  5993  nnmcl  6580  xpsnen  6931  pw1fin  7022  xpfi  7044  snexxph  7067  ctssdclemn0  7227  nninfisollemne  7248  nninfisol  7250  exmidonfinlem  7317  pw1on  7357  indpi  7475  nq0m0r  7589  genpelxp  7644  un0mulcl  9349  znegcl  9423  zeo  9498  eqreznegel  9755  xnegcl  9974  modqid0  10517  q2txmodxeq0  10551  ser0  10700  expcllem  10717  m1expcl2  10728  nn0ltexp2  10876  bcval  10916  bccl  10934  hashinfom  10945  lswex  11067  pfxclz  11155  pfxwrdsymbg  11166  cats1un  11197  resqrexlemlo  11399  iserge0  11729  sumrbdclem  11763  fsum3cvg  11764  summodclem3  11766  summodclem2a  11767  fisumss  11778  binom  11870  bcxmas  11875  prodf1  11928  prodrbdclem  11957  fproddccvg  11958  prodmodclem2a  11962  fprodntrivap  11970  prodssdc  11975  fprodssdc  11976  gcdval  12355  gcdcl  12362  lcmcl  12469  pcxnn0cl  12708  pcxcl  12709  pcmptcl  12740  infpnlem2  12758  zgz  12771  4sqlem19  12807  znf1o  14488  ssblps  14972  ssbl  14973  xmeter  14983  blssioo  15100  elply  15281  plycj  15308  1sgmprm  15541  lgslem4  15555  lgsne0  15590  2sqlem9  15676  2sqlem10  15677  bj-charfun  15881  012of  16069  2o01f  16070  nninfsellemeqinf  16094  nninffeq  16098  trilpolemclim  16116  iswomni0  16131