Step 
Hyp 
Ref 
Expression 
1 

mbfmf.1 
⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra ) 
2 

mbfmf.2 
⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra ) 
3 

mbfmf.3 
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ) 
4 

mbfmcnvima.4 
⊢ ( 𝜑 → 𝐴 ∈ 𝑇 ) 
5 

imaeq2 
⊢ ( 𝑥 = 𝐴 → ( ^{◡} 𝐹 “ 𝑥 ) = ( ^{◡} 𝐹 “ 𝐴 ) ) 
6 
5

eleq1d 
⊢ ( 𝑥 = 𝐴 → ( ( ^{◡} 𝐹 “ 𝑥 ) ∈ 𝑆 ↔ ( ^{◡} 𝐹 “ 𝐴 ) ∈ 𝑆 ) ) 
7 
1 2

ismbfm 
⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑆 MblFnM 𝑇 ) ↔ ( 𝐹 ∈ ( ∪ 𝑇 ↑_{m} ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ^{◡} 𝐹 “ 𝑥 ) ∈ 𝑆 ) ) ) 
8 
3 7

mpbid 
⊢ ( 𝜑 → ( 𝐹 ∈ ( ∪ 𝑇 ↑_{m} ∪ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑇 ( ^{◡} 𝐹 “ 𝑥 ) ∈ 𝑆 ) ) 
9 
8

simprd 
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑇 ( ^{◡} 𝐹 “ 𝑥 ) ∈ 𝑆 ) 
10 
6 9 4

rspcdva 
⊢ ( 𝜑 → ( ^{◡} 𝐹 “ 𝐴 ) ∈ 𝑆 ) 