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 φ A B = x ∈ A | φ ∪ x ∈ B | ¬ φ

Proof

Step Hyp Ref Expression
1 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
2 1 anbi1d ⊢ x = y → x ∈ A ∧ φ ↔ y ∈ A ∧ φ
3 eleq1w ⊢ x = y → x ∈ B ↔ y ∈ B
4 3 anbi1d ⊢ x = y → x ∈ B ∧ ¬ φ ↔ y ∈ B ∧ ¬ φ
5 2 4 unabw ⊢ x | x ∈ A ∧ φ ∪ x | x ∈ B ∧ ¬ φ = y | y ∈ A ∧ φ ∨ y ∈ B ∧ ¬ φ
6 df-rab ⊢ x ∈ A | φ = x | x ∈ A ∧ φ
7 df-rab ⊢ x ∈ B | ¬ φ = x | x ∈ B ∧ ¬ φ
8 6 7 uneq12i ⊢ x ∈ A | φ ∪ x ∈ B | ¬ φ = x | x ∈ A ∧ φ ∪ x | x ∈ B ∧ ¬ φ
9 df-if ⊢ if φ A B = y | y ∈ A ∧ φ ∨ y ∈ B ∧ ¬ φ
10 5 8 9 3eqtr4ri ⊢ if φ A B = x ∈ A | φ ∪ x ∈ B | ¬ φ