Metamath Proof Explorer

Theorem aovprc

Description: The value of an operation when the one of the arguments is a proper class, analogous to ovprc . (Contributed by Alexander van der Vekens, 26-May-2017)

		Ref	Expression
	Hypothesis	aovprc.1	$⊢ Rel dom F$
	Assertion	aovprc	$⊢ \neg (A \in V \land B \in V) \to ((A F B)) = V$

Proof

Step	Hyp	Ref	Expression
1		aovprc.1	$⊢ Rel dom F$
2		df-aov	$⊢ ((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		ndmafv	$⊢ \neg ⟨A, B⟩ \in dom F \to (F''' ⟨A, B⟩) = V$
7	5 6	nsyl5	$⊢ \neg (A \in V \land B \in V) \to (F''' ⟨A, B⟩) = V$
8	2 7	syl5eq	$⊢ \neg (A \in V \land B \in V) \to ((A F B)) = V$