Theorem 1st2ndb

Description: Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014)

	Ref	Expression
Assertion	1st2ndb	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
2		id	$$⊢A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
3		fvex	$$⊢1^{st}\left(A\right)\in \mathrm{V}$$
4		fvex	$$⊢2^{nd}\left(A\right)\in \mathrm{V}$$
5	3 4	opelvv	$$⊢⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
6	2 5	eqeltrdi	$$⊢A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\to A\in \left(\mathrm{V}\times \mathrm{V}\right)$$
7	1 6	impbii	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$