Theorem nfima 6023

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 5636	. 2 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
2		nfima.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfima.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfres 5936	. . 3 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)
5	4	nfrn 5898	. 2 ⊢ Ⅎ𝑥ran (𝐴 ↾ 𝐵)
6	1, 5	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝐴 “ 𝐵)

Syntax hints:  Ⅎwnfc 2876  ran crn 5624   ↾ cres 5625   “ cima 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636

This theorem is referenced by:  nfimad  6024  csbima12  6034  nfpred  6258  nfsup  9360  nfoi  9425  nfseq  13936  gsum2d2  19871  ptbasfi  23484  mbfposr  25569  itg1climres  25631  limciun  25811  nfseqs  28204  funimass4f  32594  poimirlem16  37618  poimirlem19  37621  aomclem8  43037  areaquad  43192  nfcoll  44232  binomcxplemdvbinom  44329  binomcxplemdvsum  44331  binomcxplemnotnn0  44332  rfcnpre1  45000  rfcnpre2  45012  smfpimcc  46793