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 | |- ( ph -> if ( ph , A , B ) = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfif2 | |- if ( ph , A , B ) = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } |
|
| 2 | dedlem0a | |- ( ph -> ( x e. A <-> ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) ) ) |
|
| 3 | 2 | abbi2dv | |- ( ph -> A = { x | ( ( x e. B -> ph ) -> ( x e. A /\ ph ) ) } ) |
| 4 | 1 3 | eqtr4id | |- ( ph -> if ( ph , A , B ) = A ) |