Theorem dfopif

Description: Rewrite df-op using if . When both arguments are sets, it reduces to the standard Kuratowski definition; otherwise, it is defined to be the empty set. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction. (Contributed by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.)

	Ref	Expression
Assertion	dfopif	|- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )

Proof

Step	Hyp	Ref	Expression
1		df-op	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
2		df-3an	|- ( ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) <-> ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) )
3	2	abbii	|- { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) } = { x | ( ( A e. _V /\ B e. _V ) /\ x e. { { 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		ibar	|- ( ( A e. _V /\ B e. _V ) -> ( x e. { { A } , { A , B } } <-> ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) ) )
6	5	abbi2dv	|- ( ( A e. _V /\ B e. _V ) -> { { A } , { A , B } } = { x | ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) } )
7	4 6	eqtr2d	|- ( ( A e. _V /\ B e. _V ) -> { x | ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) } = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) )
8		pm2.21	|- ( -. ( A e. _V /\ B e. _V ) -> ( ( A e. _V /\ B e. _V ) -> x e. (/) ) )
9	8	adantrd	|- ( -. ( A e. _V /\ B e. _V ) -> ( ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) -> x e. (/) ) )
10	9	abssdv	|- ( -. ( A e. _V /\ B e. _V ) -> { x | ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) } C_ (/) )
11		ss0	|- ( { x | ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) } C_ (/) -> { x | ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) } = (/) )
12	10 11	syl	|- ( -. ( A e. _V /\ B e. _V ) -> { x | ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) } = (/) )
13		iffalse	|- ( -. ( A e. _V /\ B e. _V ) -> if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) = (/) )
14	12 13	eqtr4d	|- ( -. ( A e. _V /\ B e. _V ) -> { x | ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) } = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) )
15	7 14	pm2.61i	|- { x | ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) } = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
16	1 3 15	3eqtri	|- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )