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

Metamath Proof Explorer

Definition df-abl

Description: Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011) (Revised by Mario Carneiro, 6-Jan-2015)

		Ref	Expression
	Assertion	df-abl	$⊢ Abel = Grp \cap CMnd$

Step	Hyp	Ref	Expression
0		cabl	$class Abel$
1		cgrp	$class Grp$
2		ccmn	$class CMnd$
3	1 2	cin	$class (Grp \cap CMnd)$
4	0 3	wceq	$wff Abel = Grp \cap CMnd$