Theorem ndmaovrcl

Description: Reverse closure law, in contrast to ndmovrcl where it is required that the operation's domain doesn't contain the empty set ( -. (/) e. S ), no additional asumption is required. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypothesis	ndmaov.1	|- dom F = ( S X. S )
Assertion	ndmaovrcl	|- ( (( A F B )) e. S -> ( A e. S /\ B e. S ) )

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	|- dom F = ( S X. S )
2		aovvdm	|- ( (( A F B )) e. S -> <. A , B >. e. dom F )
3		opelxp	|- ( <. A , B >. e. ( S X. S ) <-> ( A e. S /\ B e. S ) )
4	3	biimpi	|- ( <. A , B >. e. ( S X. S ) -> ( A e. S /\ B e. S ) )
5	4 1	eleq2s	|- ( <. A , B >. e. dom F -> ( A e. S /\ B e. S ) )
6	2 5	syl	|- ( (( A F B )) e. S -> ( A e. S /\ B e. S ) )