This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvbr0

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 = ∅

Proof

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 = ∅