Theorem dfopg

Description: Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.)

	Ref	Expression
Assertion	dfopg	|- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. V -> A e. _V )
2		elex	|- ( B e. W -> B e. _V )
3		dfopif	|- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
4		iftrue	|- ( ( A e. _V /\ B e. _V ) -> if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) = { { A } , { A , B } } )
5	3 4	syl5eq	|- ( ( A e. _V /\ B e. _V ) -> <. A , B >. = { { A } , { A , B } } )
6	1 2 5	syl2an	|- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )