Theorem fovcl

Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007)

	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		ffnov	|- ( F : ( R X. S ) --> C <-> ( F Fn ( R X. S ) /\ A. x e. R A. y e. S ( x F y ) e. C ) )
3	2	simprbi	|- ( F : ( R X. S ) --> C -> A. x e. R A. y e. S ( x F y ) e. C )
4	1 3	ax-mp	|- A. x e. R A. y e. S ( x F y ) e. C
5		oveq1	|- ( x = A -> ( x F y ) = ( A F y ) )
6	5	eleq1d	|- ( x = A -> ( ( x F y ) e. C <-> ( A F y ) e. C ) )
7		oveq2	|- ( y = B -> ( A F y ) = ( A F B ) )
8	7	eleq1d	|- ( y = B -> ( ( A F y ) e. C <-> ( A F B ) e. C ) )
9	6 8	rspc2v	|- ( ( A e. R /\ B e. S ) -> ( A. x e. R A. y e. S ( x F y ) e. C -> ( A F B ) e. C ) )
10	4 9	mpi	|- ( ( A e. R /\ B e. S ) -> ( A F B ) e. C )