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	⊢ ( 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑋 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 )
2		tz6.12i	⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) ) )
3	1 2	mpi	⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) )
4	3	necon1bi	⊢ ( ¬ 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑋 ) = ∅ )
5	4	orri	⊢ ( 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑋 ) = ∅ )