Definition df-mufs

Description: Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mufs	|- mUFS = { t e. mGFS | Fun ( mST ` t ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmufs	|- mUFS
1		vt	|- t
2		cmgfs	|- mGFS
3		cmst	|- mST
4	1	cv	|- t
5	4 3	cfv	|- ( mST ` t )
6	5	wfun	|- Fun ( mST ` t )
7	6 1 2	crab	|- { t e. mGFS | Fun ( mST ` t ) }
8	0 7	wceq	|- mUFS = { t e. mGFS | Fun ( mST ` t ) }