Theorem caovcld

Description: Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Hypotheses	caovclg.1	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in D\right)\right)\to xFy\in E$$
	caovcld.2	$$⊢\phi \to A\in C$$
	caovcld.3	$$⊢\phi \to B\in D$$
Assertion	caovcld	$$⊢\phi \to AFB\in E$$

Proof

Step	Hyp	Ref	Expression
1		caovclg.1	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in D\right)\right)\to xFy\in E$$
2		caovcld.2	$$⊢\phi \to A\in C$$
3		caovcld.3	$$⊢\phi \to B\in D$$
4		id	$$⊢\phi \to \phi$$
5	1	caovclg	$$⊢\left(\phi \wedge \left(A\in C\wedge B\in D\right)\right)\to AFB\in E$$
6	4 2 3 5	syl12anc	$$⊢\phi \to AFB\in E$$