Theorem nfima 6060

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 5664	. 2 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
2		nfima.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfima.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfres 5970	. . 3 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)
5	4	nfrn 5932	. 2 ⊢ Ⅎ𝑥ran (𝐴 ↾ 𝐵)
6	1, 5	nfcxfr 2925	1 ⊢ Ⅎ𝑥(𝐴 “ 𝐵)

Syntax hints:  Ⅎwnfc 2912  ran crn 5652   ↾ cres 5653   “ cima 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is referenced by:  nfimad  6061  csbima12  6071  nfpred  6296  nfsup  9399  nfoi  9464  nfseq  14035  gsum2d2  20032  ptbasfi  23695  mbfposr  25768  itg1climres  25830  limciun  26010  nfseqs  28434  funimass4f  32890  poimirlem16  38142  poimirlem19  38145  aomclem8  43645  areaquad  43800  nfcoll  44825  binomcxplemdvbinom  44922  binomcxplemdvsum  44924  binomcxplemnotnn0  44925  rfcnpre1  45598  rfcnpre2  45610  smfpimcc  47381