Theorem nfima 6033

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 5644	. 2 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
2		nfima.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfima.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfres 5946	. . 3 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)
5	4	nfrn 5907	. 2 ⊢ Ⅎ𝑥ran (𝐴 ↾ 𝐵)
6	1, 5	nfcxfr 2896	1 ⊢ Ⅎ𝑥(𝐴 “ 𝐵)

Syntax hints:  Ⅎwnfc 2883  ran crn 5632   ↾ cres 5633   “ cima 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  nfimad  6034  csbima12  6044  nfpred  6270  nfsup  9364  nfoi  9429  nfseq  13973  gsum2d2  19949  ptbasfi  23546  mbfposr  25619  itg1climres  25681  limciun  25861  nfseqs  28279  funimass4f  32710  poimirlem16  37957  poimirlem19  37960  aomclem8  43489  areaquad  43644  nfcoll  44683  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  rfcnpre1  45450  rfcnpre2  45462  smfpimcc  47236