Theorem eqeltrdi 2284

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eqeltrrdi  2285  snexprc  4216  onsucelsucexmidlem  4562  dcextest  4614  nnpredcl  4656  ovprc  5954  nnmcl  6536  xpsnen  6877  pw1fin  6968  xpfi  6988  snexxph  7011  ctssdclemn0  7171  nninfisollemne  7192  nninfisol  7194  exmidonfinlem  7255  pw1on  7288  indpi  7404  nq0m0r  7518  genpelxp  7573  un0mulcl  9277  znegcl  9351  zeo  9425  eqreznegel  9682  xnegcl  9901  modqid0  10424  q2txmodxeq0  10458  ser0  10607  expcllem  10624  m1expcl2  10635  nn0ltexp2  10783  bcval  10823  bccl  10841  hashinfom  10852  resqrexlemlo  11160  iserge0  11489  sumrbdclem  11523  fsum3cvg  11524  summodclem3  11526  summodclem2a  11527  fisumss  11538  binom  11630  bcxmas  11635  prodf1  11688  prodrbdclem  11717  fproddccvg  11718  prodmodclem2a  11722  fprodntrivap  11730  prodssdc  11735  fprodssdc  11736  gcdval  12099  gcdcl  12106  lcmcl  12213  pcxnn0cl  12451  pcxcl  12452  pcmptcl  12483  infpnlem2  12501  zgz  12514  4sqlem19  12550  znf1o  14150  ssblps  14604  ssbl  14605  xmeter  14615  blssioo  14732  elply  14913  plycj  14939  lgslem4  15160  lgsne0  15195  2sqlem9  15281  2sqlem10  15282  bj-charfun  15369  012of  15556  2o01f  15557  nninfsellemeqinf  15576  nninffeq  15580  trilpolemclim  15596  iswomni0  15611