Theorem eqeltrrid 2245

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 2161	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2244	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1335   ∈ wcel 2128

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153

This theorem is referenced by:  dmrnssfld  4851  cnvexg  5125  opabbrex  5867  offval  6041  resfunexgALT  6060  abrexexg  6068  abrexex2g  6070  opabex3d  6071  oprssdmm  6121  unfidisj  6868  ssfii  6920  djuexb  6990  nqprlu  7469  iccshftr  9904  iccshftl  9906  iccdil  9908  icccntr  9910  mertenslem2  11444  exprmfct  12030  ennnfonelemg  12202  0opn  12474  difopn  12578  tgrest  12639  txbasex  12727  txdis1cn  12748  cnmptid  12751  cnmptc  12752  cnmpt1st  12758  cnmpt2nd  12759  cnmpt2c  12760  hmeoima  12780  hmeocld  12782  fsumcncntop  13026