Theorem ovprc1

Description: The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004)

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

Proof

Step	Hyp	Ref	Expression
1		ovprc1.1	$$⊢\mathrm{Rel}\mathrm{dom}F$$
2		simpl	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to A\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 A\in \mathrm{V}\to AFB=\varnothing$$