Theorem nfrn 5951

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 5687	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5878	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5950	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2900	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2882  ^◡ccnv 5675  dom cdm 5676  ran crn 5677

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 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-cnv 5684  df-dm 5686  df-rn 5687

This theorem is referenced by:  nfima  6067  nff  6713  nffo  6804  fliftfun  7312  zfrep6  7945  ptbasfi  23318  utopsnneiplem  23985  restmetu  24312  itg2cnlem1  25524  acunirnmpt2  32167  acunirnmpt2f  32168  fnpreimac  32178  fsumiunle  32317  nsgqusf1olem1  32813  nsgqusf1olem3  32815  locfinreflem  33133  prodindf  33334  esumrnmpt2  33379  esumgect  33401  esum2d  33404  esumiun  33405  sigapildsys  33473  ldgenpisyslem1  33474  oms0  33609  breprexplema  33955  bnj1366  34153  exrecfnlem  36576  totbndbnd  36973  refsumcn  44029  disjrnmpt2  44198  disjf1o  44201  disjinfi  44202  choicefi  44210  rnmptbd2lem  44263  infnsuprnmpt  44265  rnmptbdlem  44270  rnmptss2  44272  rnmptssbi  44276  supxrleubrnmpt  44427  suprleubrnmpt  44443  infrnmptle  44444  infxrunb3rnmpt  44449  uzub  44452  supminfrnmpt  44466  infxrgelbrnmpt  44475  infrpgernmpt  44486  supminfxrrnmpt  44492  limsupubuz  44740  liminflelimsuplem  44802  stoweidlem27  45054  stoweidlem29  45056  stoweidlem31  45058  stoweidlem35  45062  stoweidlem59  45086  stoweidlem62  45089  stirlinglem5  45105  fourierdlem31  45165  fourierdlem80  45213  fourierdlem93  45226  sge00  45403  sge0f1o  45409  sge0gerp  45422  sge0pnffigt  45423  sge0lefi  45425  sge0ltfirp  45427  sge0resplit  45433  sge0reuz  45474  iunhoiioolem  45702  smfpimcc  45835  smfsup  45841  smfsupxr  45843  smfinf  45845  smflimsup  45855  nfafv2  46237