Theorem caovclg

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

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

Proof

Step	Hyp	Ref	Expression
1		caovclg.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 𝐹 𝑦 ) ∈ 𝐸 )
2	1	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 ( 𝑥 𝐹 𝑦 ) ∈ 𝐸 )
3		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ) = ( 𝐴 𝐹 𝑦 ) )
4	3	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐹 𝑦 ) ∈ 𝐸 ↔ ( 𝐴 𝐹 𝑦 ) ∈ 𝐸 ) )
5		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐹 𝑦 ) = ( 𝐴 𝐹 𝐵 ) )
6	5	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐹 𝑦 ) ∈ 𝐸 ↔ ( 𝐴 𝐹 𝐵 ) ∈ 𝐸 ) )
7	4 6	rspc2v	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 ( 𝑥 𝐹 𝑦 ) ∈ 𝐸 → ( 𝐴 𝐹 𝐵 ) ∈ 𝐸 ) )
8	2 7	mpan9	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐸 )