Theorem eqeltrdi 2268

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eqeltrrdi  2269  snexprc  4188  onsucelsucexmidlem  4530  dcextest  4582  nnpredcl  4624  ovprc  5912  nnmcl  6484  xpsnen  6823  pw1fin  6912  xpfi  6931  snexxph  6951  ctssdclemn0  7111  nninfisollemne  7131  nninfisol  7133  exmidonfinlem  7194  pw1on  7227  indpi  7343  nq0m0r  7457  genpelxp  7512  un0mulcl  9212  znegcl  9286  zeo  9360  eqreznegel  9616  xnegcl  9834  modqid0  10352  q2txmodxeq0  10386  ser0  10516  expcllem  10533  m1expcl2  10544  nn0ltexp2  10691  bcval  10731  bccl  10749  hashinfom  10760  resqrexlemlo  11024  iserge0  11353  sumrbdclem  11387  fsum3cvg  11388  summodclem3  11390  summodclem2a  11391  fisumss  11402  binom  11494  bcxmas  11499  prodf1  11552  prodrbdclem  11581  fproddccvg  11582  prodmodclem2a  11586  fprodntrivap  11594  prodssdc  11599  fprodssdc  11600  gcdval  11962  gcdcl  11969  lcmcl  12074  pcxnn0cl  12312  pcxcl  12313  pcmptcl  12342  infpnlem2  12360  zgz  12373  ssblps  14010  ssbl  14011  xmeter  14021  blssioo  14130  lgslem4  14489  lgsne0  14524  2sqlem9  14556  2sqlem10  14557  bj-charfun  14644  012of  14830  2o01f  14831  nninfsellemeqinf  14850  nninffeq  14854  trilpolemclim  14869  iswomni0  14884