Theorem opth2

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

	Ref	Expression
Hypotheses	opth2.1	|- C e. _V
	opth2.2	|- D e. _V
Assertion	opth2	|- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )

Proof

Step	Hyp	Ref	Expression
1		opth2.1	|- C e. _V
2		opth2.2	|- D e. _V
3		opthg2	|- ( ( C e. _V /\ D e. _V ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )
4	1 2 3	mp2an	|- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )