Theorem nfrn 5850

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 5591	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5776	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5849	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2904	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2886  ^◡ccnv 5579  dom cdm 5580  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  nfima  5966  nff  6580  nffo  6671  fliftfun  7163  zfrep6  7771  ptbasfi  22640  utopsnneiplem  23307  restmetu  23632  itg2cnlem1  24831  acunirnmpt2  30899  acunirnmpt2f  30900  fnpreimac  30910  fsumiunle  31045  nsgqusf1olem1  31500  nsgqusf1olem3  31502  locfinreflem  31692  prodindf  31891  esumrnmpt2  31936  esumgect  31958  esum2d  31961  esumiun  31962  sigapildsys  32030  ldgenpisyslem1  32031  oms0  32164  breprexplema  32510  bnj1366  32709  exrecfnlem  35477  totbndbnd  35874  refsumcn  42462  disjrnmpt2  42615  disjf1o  42618  disjinfi  42620  choicefi  42629  rnmptbd2lem  42683  infnsuprnmpt  42685  rnmptbdlem  42690  rnmptss2  42692  rnmptssbi  42696  supxrleubrnmpt  42836  suprleubrnmpt  42852  infrnmptle  42853  infxrunb3rnmpt  42858  uzub  42861  supminfrnmpt  42875  infxrgelbrnmpt  42884  infrpgernmpt  42895  supminfxrrnmpt  42901  limsupubuz  43144  liminflelimsuplem  43206  stoweidlem27  43458  stoweidlem29  43460  stoweidlem31  43462  stoweidlem35  43466  stoweidlem59  43490  stoweidlem62  43493  stirlinglem5  43509  fourierdlem31  43569  fourierdlem80  43617  fourierdlem93  43630  sge00  43804  sge0f1o  43810  sge0gerp  43823  sge0pnffigt  43824  sge0lefi  43826  sge0ltfirp  43828  sge0resplit  43834  sge0reuz  43875  iunhoiioolem  44103  smfpimcc  44228  smfsup  44234  smfsupxr  44236  smfinf  44238  smflimsup  44248  nfafv2  44597