# Metamath Proof Explorer

## Theorem mbfmcnvima

Description: The preimage by a measurable function is a measurable set. (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Hypotheses mbfmf.1
`|- ( ph -> S e. U. ran sigAlgebra )`
mbfmf.2
`|- ( ph -> T e. U. ran sigAlgebra )`
mbfmf.3
`|- ( ph -> F e. ( S MblFnM T ) )`
mbfmcnvima.4
`|- ( ph -> A e. T )`
Assertion mbfmcnvima
`|- ( ph -> ( `' F " A ) e. S )`

### Proof

Step Hyp Ref Expression
1 mbfmf.1
` |-  ( ph -> S e. U. ran sigAlgebra )`
2 mbfmf.2
` |-  ( ph -> T e. U. ran sigAlgebra )`
3 mbfmf.3
` |-  ( ph -> F e. ( S MblFnM T ) )`
4 mbfmcnvima.4
` |-  ( ph -> A e. T )`
5 imaeq2
` |-  ( x = A -> ( `' F " x ) = ( `' F " A ) )`
6 5 eleq1d
` |-  ( x = A -> ( ( `' F " x ) e. S <-> ( `' F " A ) e. S ) )`
7 1 2 ismbfm
` |-  ( ph -> ( F e. ( S MblFnM T ) <-> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) ) )`
8 3 7 mpbid
` |-  ( ph -> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) )`
9 8 simprd
` |-  ( ph -> A. x e. T ( `' F " x ) e. S )`
10 6 9 4 rspcdva
` |-  ( ph -> ( `' F " A ) e. S )`