Metamath Proof Explorer


Theorem dfopifOLD

Description: Obsolete version of dfopif as of 1-Aug-2024. (Contributed by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion dfopifOLD
|- <. 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 } } , (/) )