Theorem nfrn 5894

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 5632	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5821	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5893	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2902	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2884  ^◡ccnv 5620  dom cdm 5621  ran crn 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-sn 4575  df-pr 4577  df-op 4581  df-br 5094  df-opab 5156  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  nfima  6008  nff  6648  nffo  6739  fliftfun  7240  zfrep6  7866  ptbasfi  22839  utopsnneiplem  23506  restmetu  23833  itg2cnlem1  25033  acunirnmpt2  31284  acunirnmpt2f  31285  fnpreimac  31295  fsumiunle  31430  nsgqusf1olem1  31895  nsgqusf1olem3  31897  locfinreflem  32088  prodindf  32289  esumrnmpt2  32334  esumgect  32356  esum2d  32359  esumiun  32360  sigapildsys  32428  ldgenpisyslem1  32429  oms0  32564  breprexplema  32910  bnj1366  33108  exrecfnlem  35706  totbndbnd  36103  refsumcn  42946  disjrnmpt2  43105  disjf1o  43108  disjinfi  43110  choicefi  43119  rnmptbd2lem  43174  infnsuprnmpt  43176  rnmptbdlem  43181  rnmptss2  43183  rnmptssbi  43187  supxrleubrnmpt  43333  suprleubrnmpt  43349  infrnmptle  43350  infxrunb3rnmpt  43355  uzub  43358  supminfrnmpt  43372  infxrgelbrnmpt  43381  infrpgernmpt  43392  supminfxrrnmpt  43398  limsupubuz  43642  liminflelimsuplem  43704  stoweidlem27  43956  stoweidlem29  43958  stoweidlem31  43960  stoweidlem35  43964  stoweidlem59  43988  stoweidlem62  43991  stirlinglem5  44007  fourierdlem31  44067  fourierdlem80  44115  fourierdlem93  44128  sge00  44303  sge0f1o  44309  sge0gerp  44322  sge0pnffigt  44323  sge0lefi  44325  sge0ltfirp  44327  sge0resplit  44333  sge0reuz  44374  iunhoiioolem  44602  smfpimcc  44735  smfsup  44741  smfsupxr  44743  smfinf  44745  smflimsup  44755  nfafv2  45128