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  4274  onsucelsucexmidlem  4625  dcextest  4677  nnpredcl  4719  ovprc  6049  nnmcl  6644  xpsnen  7000  pw1fin  7095  xpfi  7117  snexxph  7140  ctssdclemn0  7300  nninfisollemne  7321  nninfisol  7323  exmidonfinlem  7394  pw1on  7434  indpi  7552  nq0m0r  7666  genpelxp  7721  un0mulcl  9426  znegcl  9500  zeo  9575  eqreznegel  9838  xnegcl  10057  modqid0  10602  q2txmodxeq0  10636  ser0  10785  expcllem  10802  m1expcl2  10813  nn0ltexp2  10961  bcval  11001  bccl  11019  hashinfom  11030  lswex  11155  pfxclz  11250  pfxwrdsymbg  11261  cats1un  11292  cats1fvn  11335  cats1fvnd  11336  resqrexlemlo  11564  iserge0  11894  sumrbdclem  11928  fsum3cvg  11929  summodclem3  11931  summodclem2a  11932  fisumss  11943  binom  12035  bcxmas  12040  prodf1  12093  prodrbdclem  12122  fproddccvg  12123  prodmodclem2a  12127  fprodntrivap  12135  prodssdc  12140  fprodssdc  12141  gcdval  12520  gcdcl  12527  lcmcl  12634  pcxnn0cl  12873  pcxcl  12874  pcmptcl  12905  infpnlem2  12923  zgz  12936  4sqlem19  12972  znf1o  14655  ssblps  15139  ssbl  15140  xmeter  15150  blssioo  15267  elply  15448  plycj  15475  1sgmprm  15708  lgslem4  15722  lgsne0  15757  2sqlem9  15843  2sqlem10  15844  uhgr0enedgfi  16075  vtxdgfi0e  16101  bj-charfun  16338  012of  16528  2o01f  16529  nninfsellemeqinf  16554  nninffeq  16558  trilpolemclim  16576  iswomni0  16591