Theorem eqeltrrid 2228

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

Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  dmrnssfld  4810  cnvexg  5084  opabbrex  5823  offval  5997  resfunexgALT  6016  abrexexg  6024  abrexex2g  6026  opabex3d  6027  oprssdmm  6077  unfidisj  6818  ssfii  6870  djuexb  6937  nqprlu  7379  iccshftr  9807  iccshftl  9809  iccdil  9811  icccntr  9813  mertenslem2  11337  exprmfct  11854  ennnfonelemg  11952  0opn  12212  difopn  12316  tgrest  12377  txbasex  12465  txdis1cn  12486  cnmptid  12489  cnmptc  12490  cnmpt1st  12496  cnmpt2nd  12497  cnmpt2c  12498  hmeoima  12518  hmeocld  12520  fsumcncntop  12764