Metamath Proof Explorer


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 abbi2dv ( 𝜑𝐴 = { 𝑥 ∣ ( ( 𝑥𝐵𝜑 ) → ( 𝑥𝐴𝜑 ) ) } )
4 1 3 eqtr4id ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )