Theorem nfrn 5977

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 5711	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5903	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5976	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2906	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2893  ^◡ccnv 5699  dom cdm 5700  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  nfima  6097  nff  6743  nffo  6833  fliftfun  7348  zfrep6  7995  ptbasfi  23610  utopsnneiplem  24277  restmetu  24604  itg2cnlem1  25816  acunirnmpt2  32678  acunirnmpt2f  32679  fnpreimac  32689  fsumiunle  32833  nsgqusf1olem1  33406  nsgqusf1olem3  33408  locfinreflem  33786  prodindf  33987  esumrnmpt2  34032  esumgect  34054  esum2d  34057  esumiun  34058  sigapildsys  34126  ldgenpisyslem1  34127  oms0  34262  breprexplema  34607  bnj1366  34805  exrecfnlem  37345  totbndbnd  37749  refsumcn  44930  disjrnmpt2  45095  disjf1o  45098  disjinfi  45099  choicefi  45107  rnmptbd2lem  45157  infnsuprnmpt  45159  rnmptbdlem  45164  rnmptss2  45166  rnmptssbi  45170  supxrleubrnmpt  45321  suprleubrnmpt  45337  infrnmptle  45338  infxrunb3rnmpt  45343  uzub  45346  supminfrnmpt  45360  infxrgelbrnmpt  45369  infrpgernmpt  45380  supminfxrrnmpt  45386  limsupubuz  45634  liminflelimsuplem  45696  stoweidlem27  45948  stoweidlem29  45950  stoweidlem31  45952  stoweidlem35  45956  stoweidlem59  45980  stoweidlem62  45983  stirlinglem5  45999  fourierdlem31  46059  fourierdlem80  46107  fourierdlem93  46120  sge00  46297  sge0f1o  46303  sge0gerp  46316  sge0pnffigt  46317  sge0lefi  46319  sge0ltfirp  46321  sge0resplit  46327  sge0reuz  46368  iunhoiioolem  46596  smfpimcc  46729  smfsup  46735  smfsupxr  46737  smfinf  46739  smflimsup  46749  nfafv2  47133