Theorem nfrn 5948

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

Syntax hints:  Ⅎwnfc 2879  ^◡ccnv 5671  dom cdm 5672  ran crn 5673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-cnv 5680  df-dm 5682  df-rn 5683

This theorem is referenced by:  nfima  6065  nff  6712  nffo  6804  fliftfun  7314  zfrep6  7952  ptbasfi  23478  utopsnneiplem  24145  restmetu  24472  itg2cnlem1  25684  acunirnmpt2  32439  acunirnmpt2f  32440  fnpreimac  32450  fsumiunle  32586  nsgqusf1olem1  33117  nsgqusf1olem3  33119  locfinreflem  33435  prodindf  33636  esumrnmpt2  33681  esumgect  33703  esum2d  33706  esumiun  33707  sigapildsys  33775  ldgenpisyslem1  33776  oms0  33911  breprexplema  34256  bnj1366  34454  exrecfnlem  36852  totbndbnd  37256  refsumcn  44386  disjrnmpt2  44555  disjf1o  44558  disjinfi  44559  choicefi  44567  rnmptbd2lem  44618  infnsuprnmpt  44620  rnmptbdlem  44625  rnmptss2  44627  rnmptssbi  44631  supxrleubrnmpt  44782  suprleubrnmpt  44798  infrnmptle  44799  infxrunb3rnmpt  44804  uzub  44807  supminfrnmpt  44821  infxrgelbrnmpt  44830  infrpgernmpt  44841  supminfxrrnmpt  44847  limsupubuz  45095  liminflelimsuplem  45157  stoweidlem27  45409  stoweidlem29  45411  stoweidlem31  45413  stoweidlem35  45417  stoweidlem59  45441  stoweidlem62  45444  stirlinglem5  45460  fourierdlem31  45520  fourierdlem80  45568  fourierdlem93  45581  sge00  45758  sge0f1o  45764  sge0gerp  45777  sge0pnffigt  45778  sge0lefi  45780  sge0ltfirp  45782  sge0resplit  45788  sge0reuz  45829  iunhoiioolem  46057  smfpimcc  46190  smfsup  46196  smfsupxr  46198  smfinf  46200  smflimsup  46210  nfafv2  46592