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

Metamath Proof Explorer

Theorem iffalse

Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999)

Ref Expression
Assertion iffalse ⊢ ¬ φ → if φ A B = B

Proof

Step Hyp Ref Expression
1 df-if ⊢ if φ A B = x | x ∈ A ∧ φ ∨ x ∈ B ∧ ¬ φ
2 dedlemb ⊢ ¬ φ → x ∈ B ↔ x ∈ A ∧ φ ∨ x ∈ B ∧ ¬ φ
3 2 eqabdv ⊢ ¬ φ → B = x | x ∈ A ∧ φ ∨ x ∈ B ∧ ¬ φ
4 1 3 eqtr4id ⊢ ¬ φ → if φ A B = B