Theorem syl5eqelr 2182

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

Hypotheses

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

Assertion

Ref	Expression
syl5eqelr	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl5eqelr

Step	Hyp	Ref	Expression
1		syl5eqelr.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2099	. 2 ⊢ 𝐴 = 𝐵
3		syl5eqelr.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	syl5eqel 2181	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1296   ∈ wcel 1445

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088  df-clel 2091

This theorem is referenced by:  dmrnssfld  4728  cnvexg  5002  opabbrex  5731  offval  5901  resfunexgALT  5919  abrexexg  5927  abrexex2g  5929  opabex3d  5930  unfidisj  6712  nqprlu  7203  iccshftr  9560  iccshftl  9562  iccdil  9564  icccntr  9566  mertenslem2  11079  exprmfct  11546  0opn  11857  difopn  11960  tgrest  12021  cnmptid  12103  cnmptc  12104