Metamath Proof Explorer

Theorem dfif6

Description: An alternate definition of the conditional operator df-if as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion dfif6 
|- if ( ph , A , B ) = ( { x e. A | ph } u. { x e. B | -. ph } )

Proof

Step Hyp Ref Expression
1 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
2 1 anbi1d 
 |-  ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ph ) ) )
3 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
4 3 anbi1d 
 |-  ( x = y -> ( ( x e. B /\ -. ph ) <-> ( y e. B /\ -. ph ) ) )
5 2 4 unabw 
 |-  ( { x | ( x e. A /\ ph ) } u. { x | ( x e. B /\ -. ph ) } ) = { y | ( ( y e. A /\ ph ) \/ ( y e. B /\ -. ph ) ) }
6 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
7 df-rab 
 |-  { x e. B | -. ph } = { x | ( x e. B /\ -. ph ) }
8 6 7 uneq12i 
 |-  ( { x e. A | ph } u. { x e. B | -. ph } ) = ( { x | ( x e. A /\ ph ) } u. { x | ( x e. B /\ -. ph ) } )
9 df-if 
 |-  if ( ph , A , B ) = { y | ( ( y e. A /\ ph ) \/ ( y e. B /\ -. ph ) ) }
10 5 8 9 3eqtr4ri 
 |-  if ( ph , A , B ) = ( { x e. A | ph } u. { x e. B | -. ph } )