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	$$⊢\underset{\_}{Ⅎ}xA$$
	nfima.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfima	$$⊢\underset{\_}{Ⅎ}xA\left[B\right]$$

Proof

Step	Hyp	Ref	Expression
1		nfima.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfima.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		df-ima	$$⊢A\left[B\right]=\mathrm{ran}\left({A\upharpoonright }_B\right)$$
4	1 2	nfres	$$⊢\underset{\_}{Ⅎ}x\left({A\upharpoonright }_B\right)$$
5	4	nfrn	$$⊢\underset{\_}{Ⅎ}x\mathrm{ran}\left({A\upharpoonright }_B\right)$$
6	3 5	nfcxfr	$$⊢\underset{\_}{Ⅎ}xA\left[B\right]$$