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

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

Proof

Step Hyp Ref Expression
1 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
2 1 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ) )
3 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
4 3 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝜑 ) ) )
5 2 4 unabw ⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) } ) = { 𝑦 ∣ ( ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝜑 ) ) }
6 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
7 df-rab ⊢ { 𝑥 ∈ 𝐵 ∣ ¬ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) }
8 6 7 uneq12i ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐵 ∣ ¬ 𝜑 } ) = ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) } )
9 df-if ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑦 ∣ ( ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝜑 ) ) }
10 5 8 9 3eqtr4ri ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐵 ∣ ¬ 𝜑 } )