Theorem nfrn 5935

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

This proof depends on syntax axioms:  Ⅎwnfc 2907  ^◡ccnv 5650  dom cdm 5651  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  nfima  6066  nff  6710  nffo  6800  fliftfun  7324  zfrep6OLD  7971  ptbasfi  23909  utopsnneiplem  24575  restmetu  24898  itg2cnlem1  26091  acunirnmpt2  33305  acunirnmpt2f  33306  fnpreimac  33315  fsumiunle  33470  prodindf  33479  nsgqusf1olem1  34014  nsgqusf1olem3  34016  locfinreflem  34522  esumrnmpt2  34750  esumgect  34772  esum2d  34775  esumiun  34776  sigapildsys  34845  ldgenpisyslem1  34846  oms0  34979  breprexplema  35309  bnj1366  35509  exrecfnlem  38411  totbndbnd  38832  modelaxreplem3  46078  refsumcn  46155  disjrnmpt2  46311  disjf1o  46314  disjinfi  46315  choicefi  46322  rnmptbd2lem  46368  infnsuprnmpt  46370  rnmptbdlem  46375  rnmptss2  46377  rnmptssbi  46380  supxrleubrnmpt  46524  suprleubrnmpt  46540  infrnmptle  46541  infxrunb3rnmpt  46546  uzub  46549  supminfrnmpt  46563  infxrgelbrnmpt  46572  infrpgernmpt  46583  supminfxrrnmpt  46589  limsupubuz  46831  liminflelimsuplem  46893  stoweidlem27  47145  stoweidlem29  47147  stoweidlem31  47149  stoweidlem35  47153  stoweidlem59  47177  stoweidlem62  47180  stirlinglem5  47196  fourierdlem31  47256  fourierdlem80  47304  fourierdlem93  47317  sge00  47494  sge0f1o  47500  sge0gerp  47513  sge0pnffigt  47514  sge0lefi  47516  sge0ltfirp  47518  sge0resplit  47524  sge0reuz  47565  iunhoiioolem  47793  smfpimcc  47926  smfsup  47932  smfsupxr  47934  smfinf  47936  smflimsup  47946  nfafv2  48396