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 ax-10 , ax-11 , ax-12 . (Revised by SN, 1-Aug-2024) (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		noel	|- -. x e. (/)
2	1	intnan	|- -. ( -. ( A e. _V /\ B e. _V ) /\ x e. (/) )
3		biorf	|- ( -. ( -. ( A e. _V /\ B e. _V ) /\ x e. (/) ) -> ( ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) <-> ( ( -. ( A e. _V /\ B e. _V ) /\ x e. (/) ) \/ ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) ) ) )
4	2 3	ax-mp	|- ( ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) <-> ( ( -. ( A e. _V /\ B e. _V ) /\ x e. (/) ) \/ ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) ) )
5		df-3an	|- ( ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) <-> ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) )
6		orcom	|- ( ( ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) \/ ( -. ( A e. _V /\ B e. _V ) /\ x e. (/) ) ) <-> ( ( -. ( A e. _V /\ B e. _V ) /\ x e. (/) ) \/ ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) ) )
7	4 5 6	3bitr4i	|- ( ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) <-> ( ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) \/ ( -. ( A e. _V /\ B e. _V ) /\ x e. (/) ) ) )
8		eleq1w	|- ( x = y -> ( x e. { { A } , { A , B } } <-> y e. { { A } , { A , B } } ) )
9	8	3anbi3d	|- ( x = y -> ( ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) <-> ( A e. _V /\ B e. _V /\ y e. { { A } , { A , B } } ) ) )
10		eleq1w	|- ( y = x -> ( y e. { { A } , { A , B } } <-> x e. { { A } , { A , B } } ) )
11	10	3anbi3d	|- ( y = x -> ( ( A e. _V /\ B e. _V /\ y e. { { A } , { A , B } } ) <-> ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) ) )
12		df-op	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
13	9 11 12	elab2gw	|- ( x e. _V -> ( x e. <. A , B >. <-> ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) ) )
14	13	elv	|- ( x e. <. A , B >. <-> ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) )
15		elif	|- ( x e. if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) <-> ( ( ( A e. _V /\ B e. _V ) /\ x e. { { A } , { A , B } } ) \/ ( -. ( A e. _V /\ B e. _V ) /\ x e. (/) ) ) )
16	7 14 15	3bitr4i	|- ( x e. <. A , B >. <-> x e. if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) )
17	16	eqriv	|- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )