Theorem nfrn 5899

Description: Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)

Hypothesis

Ref	Expression
nfrn.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfrn	⊢ Ⅎ𝑥ran 𝐴

Proof of Theorem nfrn

Step	Hyp	Ref	Expression
1		df-rn 5633	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5825	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5898	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2894	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2881  ^◡ccnv 5621  dom cdm 5622  ran crn 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  nfima  6025  nff  6656  nffo  6743  fliftfun  7256  zfrep6  7897  ptbasfi  23523  utopsnneiplem  24189  restmetu  24512  itg2cnlem1  25716  acunirnmpt2  32687  acunirnmpt2f  32688  fnpreimac  32698  fsumiunle  32859  prodindf  32893  nsgqusf1olem1  33443  nsgqusf1olem3  33445  locfinreflem  33946  esumrnmpt2  34174  esumgect  34196  esum2d  34199  esumiun  34200  sigapildsys  34268  ldgenpisyslem1  34269  oms0  34403  breprexplema  34736  bnj1366  34934  exrecfnlem  37523  totbndbnd  37929  modelaxreplem3  45163  refsumcn  45217  disjrnmpt2  45374  disjf1o  45377  disjinfi  45378  choicefi  45386  rnmptbd2lem  45434  infnsuprnmpt  45436  rnmptbdlem  45441  rnmptss2  45443  rnmptssbi  45446  supxrleubrnmpt  45592  suprleubrnmpt  45608  infrnmptle  45609  infxrunb3rnmpt  45614  uzub  45617  supminfrnmpt  45631  infxrgelbrnmpt  45640  infrpgernmpt  45651  supminfxrrnmpt  45657  limsupubuz  45899  liminflelimsuplem  45961  stoweidlem27  46213  stoweidlem29  46215  stoweidlem31  46217  stoweidlem35  46221  stoweidlem59  46245  stoweidlem62  46248  stirlinglem5  46264  fourierdlem31  46324  fourierdlem80  46372  fourierdlem93  46385  sge00  46562  sge0f1o  46568  sge0gerp  46581  sge0pnffigt  46582  sge0lefi  46584  sge0ltfirp  46586  sge0resplit  46592  sge0reuz  46633  iunhoiioolem  46861  smfpimcc  46994  smfsup  47000  smfsupxr  47002  smfinf  47004  smflimsup  47014  nfafv2  47406