Theorem ovprc2

Description: The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypothesis	ovprc1.1	$$⊢\mathrm{Rel}\mathrm{dom}F$$
Assertion	ovprc2	$$⊢\neg B\in \mathrm{V}\to AFB=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ovprc1.1	$$⊢\mathrm{Rel}\mathrm{dom}F$$
2		simpr	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to B\in \mathrm{V}$$
3	1	ovprc	$$⊢\neg \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to AFB=\varnothing$$
4	2 3	nsyl5	$$⊢\neg B\in \mathrm{V}\to AFB=\varnothing$$