Theorem opth2

Description: Ordered pair theorem. (Contributed by NM, 21-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		opth2.1	$$⊢C\in \mathrm{V}$$
2		opth2.2	$$⊢D\in \mathrm{V}$$
3		opthg2	$$⊢\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)\to \left(⟨A,B⟩=⟨C,D⟩\leftrightarrow \left(A=C\wedge B=D\right)\right)$$
4	1 2 3	mp2an	$$⊢⟨A,B⟩=⟨C,D⟩\leftrightarrow \left(A=C\wedge B=D\right)$$