Theorem fovcl

Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007) (Proof shortened by AV, 9-Mar-2025)

	Ref	Expression
Hypothesis	fovcl.1	|- F : ( R X. S ) --> C
Assertion	fovcl	|- ( ( A e. R /\ B e. S ) -> ( A F B ) e. C )

Proof

Step	Hyp	Ref	Expression
1		fovcl.1	|- F : ( R X. S ) --> C
2	1	a1i	|- ( A e. R -> F : ( R X. S ) --> C )
3	2	fovcld	|- ( ( A e. R /\ A e. R /\ B e. S ) -> ( A F B ) e. C )
4	3	3anidm12	|- ( ( A e. R /\ B e. S ) -> ( A F B ) e. C )