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

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