Theorem isanmbfm

Description: The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017) Remove hypotheses. (Revised by SN, 13-Jan-2025)

	Ref	Expression
Hypothesis	isanmbfm.1	|- ( ph -> F e. ( S MblFnM T ) )
Assertion	isanmbfm	|- ( ph -> F e. U. ran MblFnM )

Proof

Step	Hyp	Ref	Expression
1		isanmbfm.1	|- ( ph -> F e. ( S MblFnM T ) )
2		ovssunirn	|- ( S MblFnM T ) C_ U. ran MblFnM
3	2 1	sselid	|- ( ph -> F e. U. ran MblFnM )