Theorem nfrn 5907

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 5642	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5833	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5906	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2896	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2883  ^◡ccnv 5630  dom cdm 5631  ran crn 5632

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  nfima  6033  nff  6664  nffo  6751  fliftfun  7267  zfrep6OLD  7908  ptbasfi  23546  utopsnneiplem  24212  restmetu  24535  itg2cnlem1  25728  acunirnmpt2  32733  acunirnmpt2f  32734  fnpreimac  32743  fsumiunle  32902  prodindf  32922  nsgqusf1olem1  33473  nsgqusf1olem3  33475  locfinreflem  33984  esumrnmpt2  34212  esumgect  34234  esum2d  34237  esumiun  34238  sigapildsys  34306  ldgenpisyslem1  34307  oms0  34441  breprexplema  34774  bnj1366  34971  exrecfnlem  37695  totbndbnd  38110  modelaxreplem3  45407  refsumcn  45461  disjrnmpt2  45618  disjf1o  45621  disjinfi  45622  choicefi  45629  rnmptbd2lem  45677  infnsuprnmpt  45679  rnmptbdlem  45684  rnmptss2  45686  rnmptssbi  45689  supxrleubrnmpt  45834  suprleubrnmpt  45850  infrnmptle  45851  infxrunb3rnmpt  45856  uzub  45859  supminfrnmpt  45873  infxrgelbrnmpt  45882  infrpgernmpt  45893  supminfxrrnmpt  45899  limsupubuz  46141  liminflelimsuplem  46203  stoweidlem27  46455  stoweidlem29  46457  stoweidlem31  46459  stoweidlem35  46463  stoweidlem59  46487  stoweidlem62  46490  stirlinglem5  46506  fourierdlem31  46566  fourierdlem80  46614  fourierdlem93  46627  sge00  46804  sge0f1o  46810  sge0gerp  46823  sge0pnffigt  46824  sge0lefi  46826  sge0ltfirp  46828  sge0resplit  46834  sge0reuz  46875  iunhoiioolem  47103  smfpimcc  47236  smfsup  47242  smfsupxr  47244  smfinf  47246  smflimsup  47256  nfafv2  47666