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	|- Rel dom F
Assertion	ovprc2	|- ( -. B e. _V -> ( A F B ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		ovprc1.1	|- Rel dom F
2		simpr	|- ( ( A e. _V /\ B e. _V ) -> B e. _V )
3	1	ovprc	|- ( -. ( A e. _V /\ B e. _V ) -> ( A F B ) = (/) )
4	2 3	nsyl5	|- ( -. B e. _V -> ( A F B ) = (/) )