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 ⊢ Ⅎ _ x A
nfima.2 ⊢ Ⅎ _ x B
Assertion nfima ⊢ Ⅎ _ x A B

Proof

Step Hyp Ref Expression
1 nfima.1 ⊢ Ⅎ _ x A
2 nfima.2 ⊢ Ⅎ _ x B
3 df-ima ⊢ A B = ran ⁡ A ↾ B
4 1 2 nfres ⊢ Ⅎ _ x A ↾ B
5 4 nfrn ⊢ Ⅎ _ x ran ⁡ A ↾ B
6 3 5 nfcxfr ⊢ Ⅎ _ x A B