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 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 eleq1 
 |-  ( y = x -> ( y e. { { A } , { A , B } } <-> x e. { { A } , { A , B } } ) )
9 8 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 } } ) ) )
10 df-op 
 |-  <. A , B >. = { y | ( A e. _V /\ B e. _V /\ y e. { { A } , { A , B } } ) }
11 9 10 elab2g 
 |-  ( x e. _V -> ( x e. <. A , B >. <-> ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) ) )
12 11 elv 
 |-  ( x e. <. A , B >. <-> ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) )
13 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. (/) ) ) )
14 7 12 13 3bitr4i 
 |-  ( x e. <. A , B >. <-> x e. if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) )
15 14 eqriv 
 |-  <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )