Theorem ovrcl

Description: Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ovprc1.1	|- Rel dom F
2		n0i	|- ( C e. ( A F B ) -> -. ( A F B ) = (/) )
3	1	ovprc	|- ( -. ( A e. _V /\ B e. _V ) -> ( A F B ) = (/) )
4	2 3	nsyl2	|- ( C e. ( A F B ) -> ( A e. _V /\ B e. _V ) )