Theorem xpopth

Description: An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007)

	Ref	Expression
Assertion	xpopth	$$⊢\left(A\in \left(C\times D\right)\wedge B\in \left(R\times S\right)\right)\to \left(\left(1^{st}\left(A\right)=1^{st}\left(B\right)\wedge 2^{nd}\left(A\right)=2^{nd}\left(B\right)\right)\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	$$⊢A\in \left(C\times D\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
2		1st2nd2	$$⊢B\in \left(R\times S\right)\to B=⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩$$
3	1 2	eqeqan12d	$$⊢\left(A\in \left(C\times D\right)\wedge B\in \left(R\times S\right)\right)\to \left(A=B\leftrightarrow ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩=⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\right)$$
4		fvex	$$⊢1^{st}\left(A\right)\in \mathrm{V}$$
5		fvex	$$⊢2^{nd}\left(A\right)\in \mathrm{V}$$
6	4 5	opth	$$⊢⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩=⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\leftrightarrow \left(1^{st}\left(A\right)=1^{st}\left(B\right)\wedge 2^{nd}\left(A\right)=2^{nd}\left(B\right)\right)$$
7	3 6	bitr2di	$$⊢\left(A\in \left(C\times D\right)\wedge B\in \left(R\times S\right)\right)\to \left(\left(1^{st}\left(A\right)=1^{st}\left(B\right)\wedge 2^{nd}\left(A\right)=2^{nd}\left(B\right)\right)\leftrightarrow A=B\right)$$