Theorem caovcld

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

	Ref	Expression
Hypotheses	caovclg.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 𝐹 𝑦 ) ∈ 𝐸 )
	caovcld.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
	caovcld.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
Assertion	caovcld	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		caovclg.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 𝐹 𝑦 ) ∈ 𝐸 )
2		caovcld.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
3		caovcld.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
4		id	⊢ ( 𝜑 → 𝜑 )
5	1	caovclg	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐸 )
6	4 2 3 5	syl12anc	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ 𝐸 )