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	$$⊢\left(\mathrm{Rel}B\wedge A\in B\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		df-rel	$$⊢\mathrm{Rel}B\leftrightarrow B\subseteq \mathrm{V}\times \mathrm{V}$$
2		ssel2	$$⊢\left(B\subseteq \mathrm{V}\times \mathrm{V}\wedge A\in B\right)\to A\in \left(\mathrm{V}\times \mathrm{V}\right)$$
3	1 2	sylanb	$$⊢\left(\mathrm{Rel}B\wedge A\in B\right)\to A\in \left(\mathrm{V}\times \mathrm{V}\right)$$
4		1st2nd2	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
5	3 4	syl	$$⊢\left(\mathrm{Rel}B\wedge A\in B\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$