Theorem iftrue

Description: Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfif2	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) }
2		dedlem0a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
3	2	eqabdv	⊢ ( 𝜑 → 𝐴 = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) } )
4	1 3	eqtr4id	⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )