Definition df-mufs 34590

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 34580	. 2 class mUFS
2		vt	. . . . . 6 setvar 𝑡
3	2	cv 1540	. . . . 5 class 𝑡
4		cmst 34578	. . . . 5 class mST
5	3, 4	cfv 6543	. . . 4 class (mST‘𝑡)
6	5	wfun 6537	. . 3 wff Fun (mST‘𝑡)
7		cmgfs 34576	. . 3 class mGFS
8	6, 2, 7	crab 3432	. 2 class {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)}
9	1, 8	wceq 1541	1 wff mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)}

This definition is referenced by: (None)