Theorem eqeltrrid 2254

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

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  dmrnssfld  4867  cnvexg  5141  opabbrex  5886  offval  6057  resfunexgALT  6076  abrexexg  6086  abrexex2g  6088  opabex3d  6089  oprssdmm  6139  unfidisj  6887  ssfii  6939  djuexb  7009  nqprlu  7488  iccshftr  9930  iccshftl  9932  iccdil  9934  icccntr  9936  mertenslem2  11477  exprmfct  12070  infpnlem1  12289  ennnfonelemg  12336  grpidvalg  12604  0opn  12654  difopn  12758  tgrest  12819  txbasex  12907  txdis1cn  12928  cnmptid  12931  cnmptc  12932  cnmpt1st  12938  cnmpt2nd  12939  cnmpt2c  12940  hmeoima  12960  hmeocld  12962  fsumcncntop  13206