Theorem eqop

Description: Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007) (Proof shortened by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	eqop	$$⊢A\in \left(V\times W\right)\to \left(A=⟨B,C⟩\leftrightarrow \left(1^{st}\left(A\right)=B\wedge 2^{nd}\left(A\right)=C\right)\right)$$

Proof

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