This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqabdv 
 |-  ( ( 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 } } , (/) )