Theorem eqeltrdi 2329

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eqeltrrdi  2330  snexprc  4323  onsucelsucexmidlem  4676  dcextest  4728  nnpredcl  4770  ovprc  6121  nnmcl  6754  xpsnen  7119  pw1fin  7217  xpfi  7239  mapfi  7261  snexxph  7267  0fsupp  7298  ctssdclemn0  7451  nninfisollemne  7472  nninfisol  7474  exmidonfinlem  7546  pw1on  7586  indpi  7710  nq0m0r  7824  genpelxp  7879  un0mulcl  9602  znegcl  9680  zeo  9756  eqreznegel  10024  xnegcl  10245  modqid0  10802  q2txmodxeq0  10836  ser0  10985  expcllem  11002  m1expcl2  11013  nn0ltexp2  11163  bcval  11203  bccl  11221  hashinfom  11233  lswex  11372  pfxclz  11467  pfxwrdsymbg  11478  cats1un  11509  cats1fvn  11552  cats1fvnd  11553  resqrexlemlo  11795  iserge0  12128  sumrbdclem  12163  fsum3cvg  12164  summodclem3  12166  summodclem2a  12167  fisumss  12178  binom  12270  bcxmas  12275  prodf1  12328  prodrbdclem  12357  fproddccvg  12358  prodmodclem2a  12362  fprodntrivap  12370  prodssdc  12375  fprodssdc  12376  gcdval  12755  gcdcl  12762  lcmcl  12869  pcxnn0cl  13112  pcxcl  13113  pcmptcl  13144  infpnlem2  13162  zgz  13175  4sqlem19  13211  ballotfilemrval  13313  znf1o  15070  ssblps  15617  ssbl  15618  xmeter  15628  blssioo  15745  elply  15926  plycj  15953  1sgmprm  16249  lgslem4  16288  lgsne0  16323  2sqlem9  16409  2sqlem10  16410  uhgr0enedgfi  16643  vtxdgfi0e  16702  eulerpathprum  16887  bj-charfun  16999  012of  17189  2o01f  17190  nninfsellemeqinf  17225  nninffeq  17229  trilpolemclim  17252  iswomni0  17268