Theorem eqeltrdi 2295

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

Syntax hints:   → wi 4   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  eqeltrrdi  2296  snexprc  4229  onsucelsucexmidlem  4576  dcextest  4628  nnpredcl  4670  ovprc  5979  nnmcl  6566  xpsnen  6915  pw1fin  7006  xpfi  7028  snexxph  7051  ctssdclemn0  7211  nninfisollemne  7232  nninfisol  7234  exmidonfinlem  7300  pw1on  7337  indpi  7454  nq0m0r  7568  genpelxp  7623  un0mulcl  9328  znegcl  9402  zeo  9477  eqreznegel  9734  xnegcl  9953  modqid0  10493  q2txmodxeq0  10527  ser0  10676  expcllem  10693  m1expcl2  10704  nn0ltexp2  10852  bcval  10892  bccl  10910  hashinfom  10921  resqrexlemlo  11295  iserge0  11625  sumrbdclem  11659  fsum3cvg  11660  summodclem3  11662  summodclem2a  11663  fisumss  11674  binom  11766  bcxmas  11771  prodf1  11824  prodrbdclem  11853  fproddccvg  11854  prodmodclem2a  11858  fprodntrivap  11866  prodssdc  11871  fprodssdc  11872  gcdval  12251  gcdcl  12258  lcmcl  12365  pcxnn0cl  12604  pcxcl  12605  pcmptcl  12636  infpnlem2  12654  zgz  12667  4sqlem19  12703  znf1o  14384  ssblps  14868  ssbl  14869  xmeter  14879  blssioo  14996  elply  15177  plycj  15204  1sgmprm  15437  lgslem4  15451  lgsne0  15486  2sqlem9  15572  2sqlem10  15573  bj-charfun  15705  012of  15892  2o01f  15893  nninfsellemeqinf  15915  nninffeq  15919  trilpolemclim  15937  iswomni0  15952