Description: Two possibilities for the behavior of a function value. (Contributed by Stefan O'Rear, 2-Nov-2014) (Proof shortened by Mario Carneiro, 31-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fvbr0 | |- ( X F ( F ` X ) \/ ( F ` X ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- ( F ` X ) = ( F ` X ) |
|
| 2 | tz6.12i | |- ( ( F ` X ) =/= (/) -> ( ( F ` X ) = ( F ` X ) -> X F ( F ` X ) ) ) |
|
| 3 | 1 2 | mpi | |- ( ( F ` X ) =/= (/) -> X F ( F ` X ) ) |
| 4 | 3 | necon1bi | |- ( -. X F ( F ` X ) -> ( F ` X ) = (/) ) |
| 5 | 4 | orri | |- ( X F ( F ` X ) \/ ( F ` X ) = (/) ) |