Theorem nfrn 5706

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 5454	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5635	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5705	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2947	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2933  ^◡ccnv 5442  dom cdm 5443  ran crn 5444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-br 4963  df-opab 5025  df-cnv 5451  df-dm 5453  df-rn 5454

This theorem is referenced by:  nfima  5814  nff  6378  nffo  6457  fliftfun  6928  zfrep6  7512  ptbasfi  21873  utopsnneiplem  22539  restmetu  22863  itg2cnlem1  24045  acunirnmpt2  30095  acunirnmpt2f  30096  fnpreimac  30106  fsumiunle  30229  locfinreflem  30721  prodindf  30899  esumrnmpt2  30944  esumgect  30966  esum2d  30969  esumiun  30970  sigapildsys  31038  ldgenpisyslem1  31039  oms0  31172  breprexplema  31518  bnj1366  31718  exrecfnlem  34191  totbndbnd  34599  refsumcn  40826  suprnmpt  40970  disjrnmpt2  40989  disjf1o  40992  disjinfi  40994  choicefi  41003  rnmptbd2lem  41061  infnsuprnmpt  41063  rnmptbdlem  41068  rnmptss2  41070  rnmptssbi  41075  supxrleubrnmpt  41221  suprleubrnmpt  41238  infrnmptle  41239  infxrunb3rnmpt  41244  uzub  41247  supminfrnmpt  41261  infxrgelbrnmpt  41272  infrpgernmpt  41283  supminfxrrnmpt  41289  limsupubuz  41536  liminflelimsuplem  41598  stoweidlem27  41854  stoweidlem29  41856  stoweidlem31  41858  stoweidlem35  41862  stoweidlem59  41886  stoweidlem62  41889  stirlinglem5  41905  fourierdlem31  41965  fourierdlem53  41986  fourierdlem80  42013  fourierdlem93  42026  sge00  42200  sge0f1o  42206  sge0gerp  42219  sge0pnffigt  42220  sge0lefi  42222  sge0ltfirp  42224  sge0resplit  42230  sge0reuz  42271  iunhoiioolem  42499  smfpimcc  42624  smfsup  42630  smfsupxr  42632  smfinf  42634  smflimsup  42644  nfafv2  42933