Theorem dfop

Description: Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	dfop.1	|- A e. _V
	dfop.2	|- B e. _V
Assertion	dfop	|- <. A , B >. = { { A } , { A , B } }

Proof

Step	Hyp	Ref	Expression
1		dfop.1	|- A e. _V
2		dfop.2	|- B e. _V
3		dfopg	|- ( ( A e. _V /\ B e. _V ) -> <. A , B >. = { { A } , { A , B } } )
4	1 2 3	mp2an	|- <. A , B >. = { { A } , { A , B } }