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 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		df-rel	⊢ ( Rel 𝐵 ↔ 𝐵 ⊆ ( V × V ) )
2		ssel2	⊢ ( ( 𝐵 ⊆ ( V × V ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ( V × V ) )
3	1 2	sylanb	⊢ ( ( Rel 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ( V × V ) )
4		1st2nd2	⊢ ( 𝐴 ∈ ( V × V ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
5	3 4	syl	⊢ ( ( Rel 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )