Definition df-mufs

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

	Ref	Expression
Assertion	df-mufs	$$⊢\mathrm{mUFS}=\left\{t\in \mathrm{mGFS}|\mathrm{Fun}\mathrm{mST}\left(t\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmufs	$$class\mathrm{mUFS}$$
1		vt	$$setvart$$
2		cmgfs	$$class\mathrm{mGFS}$$
3		cmst	$$class\mathrm{mST}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class\mathrm{mST}\left(t\right)$$
6	5	wfun	$$wff\mathrm{Fun}\mathrm{mST}\left(t\right)$$
7	6 1 2	crab	$$class\left\{t\in \mathrm{mGFS}|\mathrm{Fun}\mathrm{mST}\left(t\right)\right\}$$
8	0 7	wceq	$$wff\mathrm{mUFS}=\left\{t\in \mathrm{mGFS}|\mathrm{Fun}\mathrm{mST}\left(t\right)\right\}$$