Metamath Proof Explorer

Theorem caovclg

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

Ref Expression
Hypothesis caovclg.1 ⊢ φ ∧ x ∈ C ∧ y ∈ D → x F y ∈ E
Assertion caovclg ⊢ φ ∧ A ∈ C ∧ B ∈ D → A F B ∈ E

Proof

Step Hyp Ref Expression
1 caovclg.1 ⊢ φ ∧ x ∈ C ∧ y ∈ D → x F y ∈ E
2 1 ralrimivva ⊢ φ → ∀ x ∈ C ∀ y ∈ D x F y ∈ E
3 oveq1 ⊢ x = A → x F y = A F y
4 3 eleq1d ⊢ x = A → x F y ∈ E ↔ A F y ∈ E
5 oveq2 ⊢ y = B → A F y = A F B
6 5 eleq1d ⊢ y = B → A F y ∈ E ↔ A F B ∈ E
7 4 6 rspc2v ⊢ A ∈ C ∧ B ∈ D → ∀ x ∈ C ∀ y ∈ D x F y ∈ E → A F B ∈ E
8 2 7 mpan9 ⊢ φ ∧ A ∈ C ∧ B ∈ D → A F B ∈ E