**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 𝐹 | |

Assertion | ovprc2 | ⊢ ( ¬ 𝐵 ∈ V → ( 𝐴 𝐹 𝐵 ) = ∅ ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | ovprc1.1 | ⊢ Rel dom 𝐹 | |

2 | simpr | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐵 ∈ V ) | |

3 | 1 | ovprc | ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 𝐹 𝐵 ) = ∅ ) |

4 | 2 3 | nsyl5 | ⊢ ( ¬ 𝐵 ∈ V → ( 𝐴 𝐹 𝐵 ) = ∅ ) |