Definition df-mufs 32851

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

Assertion

Ref	Expression
df-mufs	⊢ mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)}

Detailed syntax breakdown of Definition df-mufs

Step	Hyp	Ref	Expression
1		cmufs 32841	. 2 class mUFS
2		vt	. . . . . 6 setvar 𝑡
3	2	cv 1536	. . . . 5 class 𝑡
4		cmst 32839	. . . . 5 class mST
5	3, 4	cfv 6355	. . . 4 class (mST‘𝑡)
6	5	wfun 6349	. . 3 wff Fun (mST‘𝑡)
7		cmgfs 32837	. . 3 class mGFS
8	6, 2, 7	crab 3142	. 2 class {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)}
9	1, 8	wceq 1537	1 wff mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)}

This definition is referenced by: (None)