Theorem eqeltrrid 2258

Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eqeltrrid.1	⊢ 𝐵 = 𝐴
eqeltrrid.2	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
eqeltrrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrrid

Step	Hyp	Ref	Expression
1		eqeltrrid.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2174	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2257	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:  dmrnssfld  4874  cnvexg  5148  opabbrex  5897  offval  6068  resfunexgALT  6087  abrexexg  6097  abrexex2g  6099  opabex3d  6100  oprssdmm  6150  unfidisj  6899  ssfii  6951  djuexb  7021  nqprlu  7509  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  mertenslem2  11499  exprmfct  12092  infpnlem1  12311  ennnfonelemg  12358  grpidvalg  12627  0opn  12798  difopn  12902  tgrest  12963  txbasex  13051  txdis1cn  13072  cnmptid  13075  cnmptc  13076  cnmpt1st  13082  cnmpt2nd  13083  cnmpt2c  13084  hmeoima  13104  hmeocld  13106  fsumcncntop  13350