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	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )
Assertion	isanmbfm	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )

Proof

Step	Hyp	Ref	Expression
1		isanmbfm.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) )
2		ovssunirn	⊢ ( 𝑆 MblFnM 𝑇 ) ⊆ ∪ ran MblFnM
3	2 1	sselid	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )