Theorem nfrn 5936

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 5666	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5858	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5935	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2920	1 ⊢ Ⅎ𝑥ran 𝐴

This proof depends on syntax axioms:  Ⅎwnfc 2907  ^◡ccnv 5654  dom cdm 5655  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  nfima  6064  nff  6698  nffo  6788  fliftfun  7313  zfrep6OLD  7952  ptbasfi  23807  utopsnneiplem  24473  restmetu  24796  itg2cnlem1  25989  acunirnmpt2  33133  acunirnmpt2f  33134  fnpreimac  33143  fsumiunle  33299  prodindf  33308  nsgqusf1olem1  33842  nsgqusf1olem3  33844  locfinreflem  34350  esumrnmpt2  34578  esumgect  34600  esum2d  34603  esumiun  34604  sigapildsys  34673  ldgenpisyslem1  34674  oms0  34808  breprexplema  35138  bnj1366  35338  exrecfnlem  38133  totbndbnd  38539  modelaxreplem3  45803  refsumcn  45864  disjrnmpt2  46020  disjf1o  46023  disjinfi  46024  choicefi  46031  rnmptbd2lem  46077  infnsuprnmpt  46079  rnmptbdlem  46084  rnmptss2  46086  rnmptssbi  46089  supxrleubrnmpt  46234  suprleubrnmpt  46250  infrnmptle  46251  infxrunb3rnmpt  46256  uzub  46259  supminfrnmpt  46273  infxrgelbrnmpt  46282  infrpgernmpt  46293  supminfxrrnmpt  46299  limsupubuz  46541  liminflelimsuplem  46603  stoweidlem27  46855  stoweidlem29  46857  stoweidlem31  46859  stoweidlem35  46863  stoweidlem59  46887  stoweidlem62  46890  stirlinglem5  46906  fourierdlem31  46966  fourierdlem80  47014  fourierdlem93  47027  sge00  47204  sge0f1o  47210  sge0gerp  47223  sge0pnffigt  47224  sge0lefi  47226  sge0ltfirp  47228  sge0resplit  47234  sge0reuz  47275  iunhoiioolem  47503  smfpimcc  47636  smfsup  47642  smfsupxr  47644  smfinf  47646  smflimsup  47656  nfafv2  48106