Theorem nfrn 5902

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 5636	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5828	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5901	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2897	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2884  ^◡ccnv 5624  dom cdm 5625  ran crn 5626

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 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  nfima  6028  nff  6659  nffo  6746  fliftfun  7261  zfrep6OLD  7902  ptbasfi  23559  utopsnneiplem  24225  restmetu  24548  itg2cnlem1  25741  acunirnmpt2  32751  acunirnmpt2f  32752  fnpreimac  32761  fsumiunle  32920  prodindf  32940  nsgqusf1olem1  33491  nsgqusf1olem3  33493  locfinreflem  34003  esumrnmpt2  34231  esumgect  34253  esum2d  34256  esumiun  34257  sigapildsys  34325  ldgenpisyslem1  34326  oms0  34460  breprexplema  34793  bnj1366  34990  exrecfnlem  37712  totbndbnd  38127  modelaxreplem3  45428  refsumcn  45482  disjrnmpt2  45639  disjf1o  45642  disjinfi  45643  choicefi  45650  rnmptbd2lem  45698  infnsuprnmpt  45700  rnmptbdlem  45705  rnmptss2  45707  rnmptssbi  45710  supxrleubrnmpt  45855  suprleubrnmpt  45871  infrnmptle  45872  infxrunb3rnmpt  45877  uzub  45880  supminfrnmpt  45894  infxrgelbrnmpt  45903  infrpgernmpt  45914  supminfxrrnmpt  45920  limsupubuz  46162  liminflelimsuplem  46224  stoweidlem27  46476  stoweidlem29  46478  stoweidlem31  46480  stoweidlem35  46484  stoweidlem59  46508  stoweidlem62  46511  stirlinglem5  46527  fourierdlem31  46587  fourierdlem80  46635  fourierdlem93  46648  sge00  46825  sge0f1o  46831  sge0gerp  46844  sge0pnffigt  46845  sge0lefi  46847  sge0ltfirp  46849  sge0resplit  46855  sge0reuz  46896  iunhoiioolem  47124  smfpimcc  47257  smfsup  47263  smfsupxr  47265  smfinf  47267  smflimsup  47277  nfafv2  47681