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	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 𝐹 𝑦 ) ∈ 𝑆 )
Assertion	caovcl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		caovcl.1	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 𝐹 𝑦 ) ∈ 𝑆 )
2		tru	⊢ ⊤
3	1	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝐹 𝑦 ) ∈ 𝑆 )
4	3	caovclg	⊢ ( ( ⊤ ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )
5	2 4	mpan	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )