Theorem nfrn 5942

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 5678	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5869	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5941	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2893	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2875  ^◡ccnv 5666  dom cdm 5667  ran crn 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-br 5140  df-opab 5202  df-cnv 5675  df-dm 5677  df-rn 5678

This theorem is referenced by:  nfima  6058  nff  6704  nffo  6795  fliftfun  7302  zfrep6  7935  ptbasfi  23409  utopsnneiplem  24076  restmetu  24403  itg2cnlem1  25615  acunirnmpt2  32357  acunirnmpt2f  32358  fnpreimac  32368  fsumiunle  32505  nsgqusf1olem1  32996  nsgqusf1olem3  32998  locfinreflem  33312  prodindf  33513  esumrnmpt2  33558  esumgect  33580  esum2d  33583  esumiun  33584  sigapildsys  33652  ldgenpisyslem1  33653  oms0  33788  breprexplema  34133  bnj1366  34331  exrecfnlem  36751  totbndbnd  37151  refsumcn  44228  disjrnmpt2  44397  disjf1o  44400  disjinfi  44401  choicefi  44409  rnmptbd2lem  44462  infnsuprnmpt  44464  rnmptbdlem  44469  rnmptss2  44471  rnmptssbi  44475  supxrleubrnmpt  44626  suprleubrnmpt  44642  infrnmptle  44643  infxrunb3rnmpt  44648  uzub  44651  supminfrnmpt  44665  infxrgelbrnmpt  44674  infrpgernmpt  44685  supminfxrrnmpt  44691  limsupubuz  44939  liminflelimsuplem  45001  stoweidlem27  45253  stoweidlem29  45255  stoweidlem31  45257  stoweidlem35  45261  stoweidlem59  45285  stoweidlem62  45288  stirlinglem5  45304  fourierdlem31  45364  fourierdlem80  45412  fourierdlem93  45425  sge00  45602  sge0f1o  45608  sge0gerp  45621  sge0pnffigt  45622  sge0lefi  45624  sge0ltfirp  45626  sge0resplit  45632  sge0reuz  45673  iunhoiioolem  45901  smfpimcc  46034  smfsup  46040  smfsupxr  46042  smfinf  46044  smflimsup  46054  nfafv2  46436