Theorem eqop2

Description: Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		eqop2.1	$$⊢B\in \mathrm{V}$$
2		eqop2.2	$$⊢C\in \mathrm{V}$$
3	1 2	opelvv	$$⊢⟨B,C⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
4		eleq1	$$⊢A=⟨B,C⟩\to \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow ⟨B,C⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
5	3 4	mpbiri	$$⊢A=⟨B,C⟩\to A\in \left(\mathrm{V}\times \mathrm{V}\right)$$
6		eqop	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left(A=⟨B,C⟩\leftrightarrow \left(1^{st}\left(A\right)=B\wedge 2^{nd}\left(A\right)=C\right)\right)$$
7	5 6	biadanii	$$⊢A=⟨B,C⟩\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(A\right)=B\wedge 2^{nd}\left(A\right)=C\right)\right)$$