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

Metamath Proof Explorer

Theorem dfif2

Description: An alternate definition of the conditional operator df-if with one fewer connectives (but probably less intuitive to understand). (Contributed by NM, 30-Jan-2006)

Ref Expression
Assertion dfif2 
|- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }

Proof

Step Hyp Ref Expression
1 df-if 
 |-  if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2 df-or 
 |-  ( ( ( x e. B /\ -. ph ) \/ ( x e. A /\ ph ) ) <-> ( -. ( x e. B /\ -. ph ) -> ( x e. A /\ ph ) ) )
3 orcom 
 |-  ( ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) <-> ( ( x e. B /\ -. ph ) \/ ( x e. A /\ ph ) ) )
4 iman 
 |-  ( ( x e. B -> ph ) <-> -. ( x e. B /\ -. ph ) )
5 4 imbi1i 
 |-  ( ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) <-> ( -. ( x e. B /\ -. ph ) -> ( x e. A /\ ph ) ) )
6 2 3 5 3bitr4i 
 |-  ( ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) )
7 6 abbii 
 |-  { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }
8 1 7 eqtri 
 |-  if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) }