Theorem eqeltrdi 2322

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eqeltrrdi  2323  snexprc  4276  onsucelsucexmidlem  4627  dcextest  4679  nnpredcl  4721  ovprc  6053  nnmcl  6648  xpsnen  7004  pw1fin  7101  xpfi  7123  snexxph  7148  ctssdclemn0  7308  nninfisollemne  7329  nninfisol  7331  exmidonfinlem  7403  pw1on  7443  indpi  7561  nq0m0r  7675  genpelxp  7730  un0mulcl  9435  znegcl  9509  zeo  9584  eqreznegel  9847  xnegcl  10066  modqid0  10611  q2txmodxeq0  10645  ser0  10794  expcllem  10811  m1expcl2  10822  nn0ltexp2  10970  bcval  11010  bccl  11028  hashinfom  11039  lswex  11164  pfxclz  11259  pfxwrdsymbg  11270  cats1un  11301  cats1fvn  11344  cats1fvnd  11345  resqrexlemlo  11573  iserge0  11903  sumrbdclem  11937  fsum3cvg  11938  summodclem3  11940  summodclem2a  11941  fisumss  11952  binom  12044  bcxmas  12049  prodf1  12102  prodrbdclem  12131  fproddccvg  12132  prodmodclem2a  12136  fprodntrivap  12144  prodssdc  12149  fprodssdc  12150  gcdval  12529  gcdcl  12536  lcmcl  12643  pcxnn0cl  12882  pcxcl  12883  pcmptcl  12914  infpnlem2  12932  zgz  12945  4sqlem19  12981  znf1o  14664  ssblps  15148  ssbl  15149  xmeter  15159  blssioo  15276  elply  15457  plycj  15484  1sgmprm  15717  lgslem4  15731  lgsne0  15766  2sqlem9  15852  2sqlem10  15853  uhgr0enedgfi  16086  vtxdgfi0e  16145  bj-charfun  16402  012of  16592  2o01f  16593  nninfsellemeqinf  16618  nninffeq  16622  trilpolemclim  16640  iswomni0  16655