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 ) ) }