caovclg

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

		Ref	Expression
	Hypothesis	caovclg.1	$⊢ (φ \land (x \in C \land y \in D)) \to x F y \in E$
	Assertion	caovclg	$⊢ (φ \land (A \in C \land B \in D)) \to A F B \in E$

Step	Hyp	Ref	Expression
1		caovclg.1	$⊢ (φ \land (x \in C \land y \in D)) \to x F y \in E$
2	1	ralrimivva	$⊢ φ \to \forall x \in C \forall y \in D x F y \in E$
3		oveq1	$⊢ x = A \to x F y = A F y$
4	3	eleq1d	$⊢ x = A \to (x F y \in E \leftrightarrow A F y \in E)$
5		oveq2	$⊢ y = B \to A F y = A F B$
6	5	eleq1d	$⊢ y = B \to (A F y \in E \leftrightarrow A F B \in E)$
7	4 6	rspc2v	$⊢ (A \in C \land B \in D) \to (\forall x \in C \forall y \in D x F y \in E \to A F B \in E)$
8	2 7	mpan9	$⊢ (φ \land (A \in C \land B \in D)) \to A F B \in E$

Metamath Proof Explorer