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 ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 df-if if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥𝐴𝜑 ) ∨ ( 𝑥𝐵 ∧ ¬ 𝜑 ) ) }
2 dedlemb ( ¬ 𝜑 → ( 𝑥𝐵 ↔ ( ( 𝑥𝐴𝜑 ) ∨ ( 𝑥𝐵 ∧ ¬ 𝜑 ) ) ) )
3 2 abbi2dv ( ¬ 𝜑𝐵 = { 𝑥 ∣ ( ( 𝑥𝐴𝜑 ) ∨ ( 𝑥𝐵 ∧ ¬ 𝜑 ) ) } )
4 1 3 eqtr4id ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )