Metamath Proof Explorer


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 φFSMblFnμT
Assertion isanmbfm φFranMblFnμ

Proof

Step Hyp Ref Expression
1 isanmbfm.1 φFSMblFnμT
2 ovssunirn SMblFnμTranMblFnμ
3 2 1 sselid φFranMblFnμ