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		dedlemb	⊢ ( ¬ 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) ) )
2	1	abbi2dv	⊢ ( ¬ 𝜑 → 𝐵 = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) } )
3		df-if	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) }
4	2 3	syl6reqr	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )