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

Metamath Proof Explorer

Theorem 1st2nd

Description: Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006)

Ref Expression
Assertion 1st2nd ⊢ Rel ⁡ B ∧ A ∈ B → A = 1 st ⁡ A 2 nd ⁡ A

Proof

Step Hyp Ref Expression
1 df-rel ⊢ Rel ⁡ B ↔ B ⊆ V × V
2 ssel2 ⊢ B ⊆ V × V ∧ A ∈ B → A ∈ V × V
3 1 2 sylanb ⊢ Rel ⁡ B ∧ A ∈ B → A ∈ V × V
4 1st2nd2 ⊢ A ∈ V × V → A = 1 st ⁡ A 2 nd ⁡ A
5 3 4 syl ⊢ Rel ⁡ B ∧ A ∈ B → A = 1 st ⁡ A 2 nd ⁡ A