This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfima

Description: Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Hypotheses nfima.1 ⊢ Ⅎ 𝑥 𝐴
nfima.2 ⊢ Ⅎ 𝑥 𝐵
Assertion nfima Ⅎ 𝑥 ( 𝐴 “ 𝐵 )

Proof

Step Hyp Ref Expression
1 nfima.1 ⊢ Ⅎ 𝑥 𝐴
2 nfima.2 ⊢ Ⅎ 𝑥 𝐵
3 df-ima ⊢ ( 𝐴 “ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 )
4 1 2 nfres ⊢ Ⅎ 𝑥 ( 𝐴 ↾ 𝐵 )
5 4 nfrn ⊢ Ⅎ 𝑥 ran ( 𝐴 ↾ 𝐵 )
6 3 5 nfcxfr ⊢ Ⅎ 𝑥 ( 𝐴 “ 𝐵 )