Theorem nfima 6072

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 5676	. 2 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
2		nfima.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfima.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfres 5982	. . 3 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵)
5	4	nfrn 5944	. 2 ⊢ Ⅎ𝑥ran (𝐴 ↾ 𝐵)
6	1, 5	nfcxfr 2923	1 ⊢ Ⅎ𝑥(𝐴 “ 𝐵)

Syntax hints:  Ⅎwnfc 2910  ran crn 5664   ↾ cres 5665   “ cima 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is referenced by:  nfimad  6073  csbima12  6083  nfpred  6309  nfsup  9412  nfoi  9477  nfseq  14049  gsum2d2  20045  ptbasfi  23719  mbfposr  25792  itg1climres  25854  limciun  26034  nfseqs  28461  funimass4f  32963  poimirlem16  38268  poimirlem19  38271  aomclem8  43771  areaquad  43926  nfcoll  44949  binomcxplemdvbinom  45046  binomcxplemdvsum  45048  binomcxplemnotnn0  45049  rfcnpre1  45722  rfcnpre2  45734  smfpimcc  47505