Theorem nfrn 5894

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 5629	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5820	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5893	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2899	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2886  ^◡ccnv 5617  dom cdm 5618  ran crn 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  nfima  6020  nff  6651  nffo  6738  fliftfun  7256  zfrep6OLD  7897  ptbasfi  23564  utopsnneiplem  24230  restmetu  24553  itg2cnlem1  25746  acunirnmpt2  32752  acunirnmpt2f  32753  fnpreimac  32762  fsumiunle  32921  prodindf  32941  nsgqusf1olem1  33496  nsgqusf1olem3  33498  locfinreflem  34024  esumrnmpt2  34252  esumgect  34274  esum2d  34277  esumiun  34278  sigapildsys  34346  ldgenpisyslem1  34347  oms0  34481  breprexplema  34814  bnj1366  35011  exrecfnlem  37741  totbndbnd  38156  modelaxreplem3  45424  refsumcn  45478  disjrnmpt2  45635  disjf1o  45638  disjinfi  45639  choicefi  45646  rnmptbd2lem  45692  infnsuprnmpt  45694  rnmptbdlem  45699  rnmptss2  45701  rnmptssbi  45704  supxrleubrnmpt  45849  suprleubrnmpt  45865  infrnmptle  45866  infxrunb3rnmpt  45871  uzub  45874  supminfrnmpt  45888  infxrgelbrnmpt  45897  infrpgernmpt  45908  supminfxrrnmpt  45914  limsupubuz  46156  liminflelimsuplem  46218  stoweidlem27  46470  stoweidlem29  46472  stoweidlem31  46474  stoweidlem35  46478  stoweidlem59  46502  stoweidlem62  46505  stirlinglem5  46521  fourierdlem31  46581  fourierdlem80  46629  fourierdlem93  46642  sge00  46819  sge0f1o  46825  sge0gerp  46838  sge0pnffigt  46839  sge0lefi  46841  sge0ltfirp  46843  sge0resplit  46849  sge0reuz  46890  iunhoiioolem  47118  smfpimcc  47251  smfsup  47257  smfsupxr  47259  smfinf  47261  smflimsup  47271  nfafv2  47681