Theorem nfrn 5965

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

Syntax hints:  Ⅎwnfc 2887  ^◡ccnv 5687  dom cdm 5688  ran crn 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699

This theorem is referenced by:  nfima  6087  nff  6732  nffo  6819  fliftfun  7331  zfrep6  7977  ptbasfi  23604  utopsnneiplem  24271  restmetu  24598  itg2cnlem1  25810  acunirnmpt2  32676  acunirnmpt2f  32677  fnpreimac  32687  fsumiunle  32835  nsgqusf1olem1  33420  nsgqusf1olem3  33422  locfinreflem  33800  prodindf  34003  esumrnmpt2  34048  esumgect  34070  esum2d  34073  esumiun  34074  sigapildsys  34142  ldgenpisyslem1  34143  oms0  34278  breprexplema  34623  bnj1366  34821  exrecfnlem  37361  totbndbnd  37775  modelaxreplem3  44944  refsumcn  44967  disjrnmpt2  45130  disjf1o  45133  disjinfi  45134  choicefi  45142  rnmptbd2lem  45192  infnsuprnmpt  45194  rnmptbdlem  45199  rnmptss2  45201  rnmptssbi  45205  supxrleubrnmpt  45355  suprleubrnmpt  45371  infrnmptle  45372  infxrunb3rnmpt  45377  uzub  45380  supminfrnmpt  45394  infxrgelbrnmpt  45403  infrpgernmpt  45414  supminfxrrnmpt  45420  limsupubuz  45668  liminflelimsuplem  45730  stoweidlem27  45982  stoweidlem29  45984  stoweidlem31  45986  stoweidlem35  45990  stoweidlem59  46014  stoweidlem62  46017  stirlinglem5  46033  fourierdlem31  46093  fourierdlem80  46141  fourierdlem93  46154  sge00  46331  sge0f1o  46337  sge0gerp  46350  sge0pnffigt  46351  sge0lefi  46353  sge0ltfirp  46355  sge0resplit  46361  sge0reuz  46402  iunhoiioolem  46630  smfpimcc  46763  smfsup  46769  smfsupxr  46771  smfinf  46773  smflimsup  46783  nfafv2  47167