Definition df-mufs 33566

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 33556	. 2 class mUFS
2		vt	. . . . . 6 setvar 𝑡
3	2	cv 1538	. . . . 5 class 𝑡
4		cmst 33554	. . . . 5 class mST
5	3, 4	cfv 6433	. . . 4 class (mST‘𝑡)
6	5	wfun 6427	. . 3 wff Fun (mST‘𝑡)
7		cmgfs 33552	. . 3 class mGFS
8	6, 2, 7	crab 3068	. 2 class {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)}
9	1, 8	wceq 1539	1 wff mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)}

This definition is referenced by: (None)