Theorem nfima 5632

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

Hypotheses

Ref	Expression
nfima.1	⊢ Ⅎ𝑥𝐴
nfima.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfima	⊢ Ⅎ𝑥(𝐴 “ 𝐵)

Proof of Theorem nfima

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

Syntax hints:  Ⅎwnfc 2889  ran crn 5267   ↾ cres 5268   “ cima 5269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279

This theorem is referenced by:  nfimad  5633  csbima12  5641  nfpred  5846  nfsup  8524  nfoi  8586  nfseq  13025  gsum2d2  18593  ptbasfi  21606  mbfposr  23638  itg1climres  23700  limciun  23877  funimass4f  29767  poimirlem16  33756  poimirlem19  33759  aomclem8  38151  areaquad  38322  binomcxplemdvbinom  39072  binomcxplemdvsum  39074  binomcxplemnotnn0  39075  rfcnpre1  39695  rfcnpre2  39707  smfpimcc  41538