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	$$⊢\left(x\in S\wedge y\in S\right)\to xFy\in S$$
Assertion	caovcl	$$⊢\left(A\in S\wedge B\in S\right)\to AFB\in S$$

Proof

Step	Hyp	Ref	Expression
1		caovcl.1	$$⊢\left(x\in S\wedge y\in S\right)\to xFy\in S$$
2		tru	$$⊢\top$$
3	1	adantl	$$⊢\left(\top \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy\in S$$
4	3	caovclg	$$⊢\left(\top \wedge \left(A\in S\wedge B\in S\right)\right)\to AFB\in S$$
5	2 4	mpan	$$⊢\left(A\in S\wedge B\in S\right)\to AFB\in S$$