This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (x \in S \land y \in S) \to x F y \in S$
	Assertion	caovcl	$⊢ (A \in S \land B \in S) \to A F B \in S$

Step	Hyp	Ref	Expression
1		caovcl.1	$⊢ (x \in S \land y \in S) \to x F y \in S$
2		tru	$⊢ ⊤$
3	1	adantl	$⊢ (⊤ \land (x \in S \land y \in S)) \to x F y \in S$
4	3	caovclg	$⊢ (⊤ \land (A \in S \land B \in S)) \to A F B \in S$
5	2 4	mpan	$⊢ (A \in S \land B \in S) \to A F B \in S$