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  4575  dcextest  4627  nnpredcl  4669  ovprc  5970  nnmcl  6557  xpsnen  6898  pw1fin  6989  xpfi  7011  snexxph  7034  ctssdclemn0  7194  nninfisollemne  7215  nninfisol  7217  exmidonfinlem  7283  pw1on  7320  indpi  7437  nq0m0r  7551  genpelxp  7606  un0mulcl  9311  znegcl  9385  zeo  9460  eqreznegel  9717  xnegcl  9936  modqid0  10476  q2txmodxeq0  10510  ser0  10659  expcllem  10676  m1expcl2  10687  nn0ltexp2  10835  bcval  10875  bccl  10893  hashinfom  10904  resqrexlemlo  11243  iserge0  11573  sumrbdclem  11607  fsum3cvg  11608  summodclem3  11610  summodclem2a  11611  fisumss  11622  binom  11714  bcxmas  11719  prodf1  11772  prodrbdclem  11801  fproddccvg  11802  prodmodclem2a  11806  fprodntrivap  11814  prodssdc  11819  fprodssdc  11820  gcdval  12199  gcdcl  12206  lcmcl  12313  pcxnn0cl  12552  pcxcl  12553  pcmptcl  12584  infpnlem2  12602  zgz  12615  4sqlem19  12651  znf1o  14331  ssblps  14815  ssbl  14816  xmeter  14826  blssioo  14943  elply  15124  plycj  15151  1sgmprm  15384  lgslem4  15398  lgsne0  15433  2sqlem9  15519  2sqlem10  15520  bj-charfun  15607  012of  15794  2o01f  15795  nninfsellemeqinf  15817  nninffeq  15821  trilpolemclim  15839  iswomni0  15854