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 2897	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2884  ^◡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 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 2709

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 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  nfima  6025  nff  6656  nffo  6743  fliftfun  7258  zfrep6OLD  7899  ptbasfi  23524  utopsnneiplem  24190  restmetu  24513  itg2cnlem1  25706  acunirnmpt2  32722  acunirnmpt2f  32723  fnpreimac  32732  fsumiunle  32893  prodindf  32927  nsgqusf1olem1  33478  nsgqusf1olem3  33480  locfinreflem  33990  esumrnmpt2  34218  esumgect  34240  esum2d  34243  esumiun  34244  sigapildsys  34312  ldgenpisyslem1  34313  oms0  34447  breprexplema  34780  bnj1366  34977  exrecfnlem  37691  totbndbnd  38101  modelaxreplem3  45410  refsumcn  45464  disjrnmpt2  45621  disjf1o  45624  disjinfi  45625  choicefi  45632  rnmptbd2lem  45680  infnsuprnmpt  45682  rnmptbdlem  45687  rnmptss2  45689  rnmptssbi  45692  supxrleubrnmpt  45838  suprleubrnmpt  45854  infrnmptle  45855  infxrunb3rnmpt  45860  uzub  45863  supminfrnmpt  45877  infxrgelbrnmpt  45886  infrpgernmpt  45897  supminfxrrnmpt  45903  limsupubuz  46145  liminflelimsuplem  46207  stoweidlem27  46459  stoweidlem29  46461  stoweidlem31  46463  stoweidlem35  46467  stoweidlem59  46491  stoweidlem62  46494  stirlinglem5  46510  fourierdlem31  46570  fourierdlem80  46618  fourierdlem93  46631  sge00  46808  sge0f1o  46814  sge0gerp  46827  sge0pnffigt  46828  sge0lefi  46830  sge0ltfirp  46832  sge0resplit  46838  sge0reuz  46879  iunhoiioolem  47107  smfpimcc  47240  smfsup  47246  smfsupxr  47248  smfinf  47250  smflimsup  47260  nfafv2  47652