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	$$⊢\left(XFF\left(X\right)\vee F\left(X\right)=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢F\left(X\right)=F\left(X\right)$$
2		tz6.12i	$$⊢F\left(X\right)\ne \varnothing \to \left(F\left(X\right)=F\left(X\right)\to XFF\left(X\right)\right)$$
3	1 2	mpi	$$⊢F\left(X\right)\ne \varnothing \to XFF\left(X\right)$$
4	3	necon1bi	$$⊢\neg XFF\left(X\right)\to F\left(X\right)=\varnothing$$
5	4	orri	$$⊢\left(XFF\left(X\right)\vee F\left(X\right)=\varnothing \right)$$