Theorem aovrcl

Description: Reverse closure for an operation value, analogous to afvvv . In contrast to ovrcl , elementhood of the operation's value in a set is required, not containing an element. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypothesis	aovprc.1	|- Rel dom F
Assertion	aovrcl	|- ( (( A F B )) e. C -> ( A e. _V /\ B e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		aovprc.1	|- Rel dom F
2		df-aov	|- (( A F B )) = ( F ''' <. A , B >. )
3	2	eleq1i	|- ( (( A F B )) e. C <-> ( F ''' <. A , B >. ) e. C )
4		afvvdm	|- ( ( F ''' <. A , B >. ) e. C -> <. A , B >. e. dom F )
5		df-br	|- ( A dom F B <-> <. A , B >. e. dom F )
6	1	brrelex12i	|- ( A dom F B -> ( A e. _V /\ B e. _V ) )
7	5 6	sylbir	|- ( <. A , B >. e. dom F -> ( A e. _V /\ B e. _V ) )
8	4 7	syl	|- ( ( F ''' <. A , B >. ) e. C -> ( A e. _V /\ B e. _V ) )
9	3 8	sylbi	|- ( (( A F B )) e. C -> ( A e. _V /\ B e. _V ) )