ovprc

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 F$
	Assertion	ovprc	$⊢ \neg (A \in V \land B \in V) \to A F B = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		ovprc1.1	$⊢ Rel dom F$
2		df-ov	$⊢ A F B = F (⟨A, B⟩)$
3		df-br	$⊢ A dom F B \leftrightarrow ⟨A, B⟩ \in dom F$
4	1	brrelex12i	$⊢ A dom F B \to (A \in V \land B \in V)$
5	3 4	sylbir	$⊢ ⟨A, B⟩ \in dom F \to (A \in V \land B \in V)$
6	5	con3i	$⊢ \neg (A \in V \land B \in V) \to \neg ⟨A, B⟩ \in dom F$
7		ndmfv	$⊢ \neg ⟨A, B⟩ \in dom F \to F (⟨A, B⟩) = \emptyset$
8	6 7	syl	$⊢ \neg (A \in V \land B \in V) \to F (⟨A, B⟩) = \emptyset$
9	2 8	syl5eq	$⊢ \neg (A \in V \land B \in V) \to A F B = \emptyset$

Metamath Proof Explorer

Theorem ovprc

Proof