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

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | dfif2 | ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) } | |

2 | dedlem0a | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) ) | |

3 | 2 | abbi2dv | ⊢ ( 𝜑 → 𝐴 = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐵 → 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) } ) |

4 | 1 3 | eqtr4id | ⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ) |