This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eleq1a

Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994)

Ref Expression
Assertion eleq1a ⊢ A ∈ B → C = A → C ∈ B

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ C = A → C ∈ B ↔ A ∈ B
2 1 biimprcd ⊢ A ∈ B → C = A → C ∈ B