Theorem ovrcl

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

	Ref	Expression
Hypothesis	ovprc1.1	⊢ Rel dom 𝐹
Assertion	ovrcl	⊢ ( 𝐶 ∈ ( 𝐴 𝐹 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		ovprc1.1	⊢ Rel dom 𝐹
2		n0i	⊢ ( 𝐶 ∈ ( 𝐴 𝐹 𝐵 ) → ¬ ( 𝐴 𝐹 𝐵 ) = ∅ )
3	1	ovprc	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 𝐹 𝐵 ) = ∅ )
4	2 3	nsyl2	⊢ ( 𝐶 ∈ ( 𝐴 𝐹 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )