Theorem opthg2

Description: Ordered pair theorem. (Contributed by NM, 14-Oct-2005) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	opthg2	$$⊢\left(C\in V\wedge D\in W\right)\to \left(⟨A,B⟩=⟨C,D⟩\leftrightarrow \left(A=C\wedge B=D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		opthg	$$⊢\left(C\in V\wedge D\in W\right)\to \left(⟨C,D⟩=⟨A,B⟩\leftrightarrow \left(C=A\wedge D=B\right)\right)$$
2		eqcom	$$⊢⟨A,B⟩=⟨C,D⟩\leftrightarrow ⟨C,D⟩=⟨A,B⟩$$
3		eqcom	$$⊢A=C\leftrightarrow C=A$$
4		eqcom	$$⊢B=D\leftrightarrow D=B$$
5	3 4	anbi12i	$$⊢\left(A=C\wedge B=D\right)\leftrightarrow \left(C=A\wedge D=B\right)$$
6	1 2 5	3bitr4g	$$⊢\left(C\in V\wedge D\in W\right)\to \left(⟨A,B⟩=⟨C,D⟩\leftrightarrow \left(A=C\wedge B=D\right)\right)$$