Theorem eqeltrdi 2320

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrrdi  2321  snexprc  4269  onsucelsucexmidlem  4620  dcextest  4672  nnpredcl  4714  ovprc  6036  nnmcl  6625  xpsnen  6976  pw1fin  7068  xpfi  7090  snexxph  7113  ctssdclemn0  7273  nninfisollemne  7294  nninfisol  7296  exmidonfinlem  7367  pw1on  7407  indpi  7525  nq0m0r  7639  genpelxp  7694  un0mulcl  9399  znegcl  9473  zeo  9548  eqreznegel  9805  xnegcl  10024  modqid0  10567  q2txmodxeq0  10601  ser0  10750  expcllem  10767  m1expcl2  10778  nn0ltexp2  10926  bcval  10966  bccl  10984  hashinfom  10995  lswex  11118  pfxclz  11206  pfxwrdsymbg  11217  cats1un  11248  cats1fvn  11291  cats1fvnd  11292  resqrexlemlo  11519  iserge0  11849  sumrbdclem  11883  fsum3cvg  11884  summodclem3  11886  summodclem2a  11887  fisumss  11898  binom  11990  bcxmas  11995  prodf1  12048  prodrbdclem  12077  fproddccvg  12078  prodmodclem2a  12082  fprodntrivap  12090  prodssdc  12095  fprodssdc  12096  gcdval  12475  gcdcl  12482  lcmcl  12589  pcxnn0cl  12828  pcxcl  12829  pcmptcl  12860  infpnlem2  12878  zgz  12891  4sqlem19  12927  znf1o  14609  ssblps  15093  ssbl  15094  xmeter  15104  blssioo  15221  elply  15402  plycj  15429  1sgmprm  15662  lgslem4  15676  lgsne0  15711  2sqlem9  15797  2sqlem10  15798  bj-charfun  16128  012of  16316  2o01f  16317  nninfsellemeqinf  16341  nninffeq  16345  trilpolemclim  16363  iswomni0  16378