Theorem nfrn 5901

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 5635	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5827	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5900	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2896	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2883  ^◡ccnv 5623  dom cdm 5624  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  nfima  6027  nff  6658  nffo  6745  fliftfun  7258  zfrep6  7899  ptbasfi  23525  utopsnneiplem  24191  restmetu  24514  itg2cnlem1  25718  acunirnmpt2  32738  acunirnmpt2f  32739  fnpreimac  32749  fsumiunle  32910  prodindf  32944  nsgqusf1olem1  33494  nsgqusf1olem3  33496  locfinreflem  33997  esumrnmpt2  34225  esumgect  34247  esum2d  34250  esumiun  34251  sigapildsys  34319  ldgenpisyslem1  34320  oms0  34454  breprexplema  34787  bnj1366  34985  exrecfnlem  37584  totbndbnd  37990  modelaxreplem3  45221  refsumcn  45275  disjrnmpt2  45432  disjf1o  45435  disjinfi  45436  choicefi  45444  rnmptbd2lem  45492  infnsuprnmpt  45494  rnmptbdlem  45499  rnmptss2  45501  rnmptssbi  45504  supxrleubrnmpt  45650  suprleubrnmpt  45666  infrnmptle  45667  infxrunb3rnmpt  45672  uzub  45675  supminfrnmpt  45689  infxrgelbrnmpt  45698  infrpgernmpt  45709  supminfxrrnmpt  45715  limsupubuz  45957  liminflelimsuplem  46019  stoweidlem27  46271  stoweidlem29  46273  stoweidlem31  46275  stoweidlem35  46279  stoweidlem59  46303  stoweidlem62  46306  stirlinglem5  46322  fourierdlem31  46382  fourierdlem80  46430  fourierdlem93  46443  sge00  46620  sge0f1o  46626  sge0gerp  46639  sge0pnffigt  46640  sge0lefi  46642  sge0ltfirp  46644  sge0resplit  46650  sge0reuz  46691  iunhoiioolem  46919  smfpimcc  47052  smfsup  47058  smfsupxr  47060  smfinf  47062  smflimsup  47072  nfafv2  47464