Theorem eqeltrdi 2261

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

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eqeltrrdi  2262  snexprc  4172  onsucelsucexmidlem  4513  dcextest  4565  nnpredcl  4607  ovprc  5888  nnmcl  6460  xpsnen  6799  pw1fin  6888  xpfi  6907  snexxph  6927  ctssdclemn0  7087  nninfisollemne  7107  nninfisol  7109  exmidonfinlem  7170  pw1on  7203  indpi  7304  nq0m0r  7418  genpelxp  7473  un0mulcl  9169  znegcl  9243  zeo  9317  eqreznegel  9573  xnegcl  9789  modqid0  10306  q2txmodxeq0  10340  ser0  10470  expcllem  10487  m1expcl2  10498  nn0ltexp2  10644  bcval  10683  bccl  10701  hashinfom  10712  resqrexlemlo  10977  iserge0  11306  sumrbdclem  11340  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  fisumss  11355  binom  11447  bcxmas  11452  prodf1  11505  prodrbdclem  11534  fproddccvg  11535  prodmodclem2a  11539  fprodntrivap  11547  prodssdc  11552  fprodssdc  11553  gcdval  11914  gcdcl  11921  lcmcl  12026  pcxnn0cl  12264  pcxcl  12265  pcmptcl  12294  infpnlem2  12312  zgz  12325  ssblps  13219  ssbl  13220  xmeter  13230  blssioo  13339  lgslem4  13698  lgsne0  13733  2sqlem9  13754  2sqlem10  13755  bj-charfun  13842  012of  14028  2o01f  14029  nninfsellemeqinf  14049  nninffeq  14053  trilpolemclim  14068  iswomni0  14083