Description: The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ovprc1.1 | ⊢ Rel dom 𝐹 | |
| Assertion | ovprc | ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 𝐹 𝐵 ) = ∅ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ovprc1.1 | ⊢ Rel dom 𝐹 | |
| 2 | df-ov | ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) | |
| 3 | df-br | ⊢ ( 𝐴 dom 𝐹 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) | |
| 4 | 1 | brrelex12i | ⊢ ( 𝐴 dom 𝐹 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| 5 | 3 4 | sylbir | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| 6 | ndmfv | ⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) | |
| 7 | 5 6 | nsyl5 | ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ) |
| 8 | 2 7 | syl5eq | ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 𝐹 𝐵 ) = ∅ ) |