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	⊢ Rel dom 𝐹
Assertion	ovprc1	⊢ ( ¬ 𝐴 ∈ V → ( 𝐴 𝐹 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ovprc1.1	⊢ Rel dom 𝐹
2		simpl	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
3	1	ovprc	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 𝐹 𝐵 ) = ∅ )
4	2 3	nsyl5	⊢ ( ¬ 𝐴 ∈ V → ( 𝐴 𝐹 𝐵 ) = ∅ )