Definition df-mufs

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmufs	⊢ mUFS
1		vt	⊢ 𝑡
2		cmgfs	⊢ mGFS
3		cmst	⊢ mST
4	1	cv	⊢ 𝑡
5	4 3	cfv	⊢ ( mST ‘ 𝑡 )
6	5	wfun	⊢ Fun ( mST ‘ 𝑡 )
7	6 1 2	crab	⊢ { 𝑡 ∈ mGFS ∣ Fun ( mST ‘ 𝑡 ) }
8	0 7	wceq	⊢ mUFS = { 𝑡 ∈ mGFS ∣ Fun ( mST ‘ 𝑡 ) }