Theorem caovcl

Description: Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995) (Revised by Mario Carneiro, 26-May-2014)

	Ref	Expression
Hypothesis	caovcl.1	|- ( ( x e. S /\ y e. S ) -> ( x F y ) e. S )
Assertion	caovcl	|- ( ( A e. S /\ B e. S ) -> ( A F B ) e. S )

Proof

Step	Hyp	Ref	Expression
1		caovcl.1	|- ( ( x e. S /\ y e. S ) -> ( x F y ) e. S )
2		tru	|- T.
3	1	adantl	|- ( ( T. /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )
4	3	caovclg	|- ( ( T. /\ ( A e. S /\ B e. S ) ) -> ( A F B ) e. S )
5	2 4	mpan	|- ( ( A e. S /\ B e. S ) -> ( A F B ) e. S )