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 ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) }

Proof

Step	Hyp	Ref	Expression
1		df-if	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) }
2		df-or	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ∨ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( ¬ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
3		orcom	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ∨ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
4		iman	⊢ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ¬ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) )
5	4	imbi1i	⊢ ( ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( ¬ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
6	2 3 5	3bitr4i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
7	6	abbii	⊢ { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) } = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) }
8	1 7	eqtri	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) }