Theorem nfrn 5963

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 5696	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5889	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5962	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2903	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2890  ^◡ccnv 5684  dom cdm 5685  ran crn 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-cnv 5693  df-dm 5695  df-rn 5696

This theorem is referenced by:  nfima  6086  nff  6732  nffo  6819  fliftfun  7332  zfrep6  7979  ptbasfi  23589  utopsnneiplem  24256  restmetu  24583  itg2cnlem1  25796  acunirnmpt2  32670  acunirnmpt2f  32671  fnpreimac  32681  fsumiunle  32831  prodindf  32848  nsgqusf1olem1  33441  nsgqusf1olem3  33443  locfinreflem  33839  esumrnmpt2  34069  esumgect  34091  esum2d  34094  esumiun  34095  sigapildsys  34163  ldgenpisyslem1  34164  oms0  34299  breprexplema  34645  bnj1366  34843  exrecfnlem  37380  totbndbnd  37796  modelaxreplem3  44997  refsumcn  45035  disjrnmpt2  45193  disjf1o  45196  disjinfi  45197  choicefi  45205  rnmptbd2lem  45255  infnsuprnmpt  45257  rnmptbdlem  45262  rnmptss2  45264  rnmptssbi  45267  supxrleubrnmpt  45417  suprleubrnmpt  45433  infrnmptle  45434  infxrunb3rnmpt  45439  uzub  45442  supminfrnmpt  45456  infxrgelbrnmpt  45465  infrpgernmpt  45476  supminfxrrnmpt  45482  limsupubuz  45728  liminflelimsuplem  45790  stoweidlem27  46042  stoweidlem29  46044  stoweidlem31  46046  stoweidlem35  46050  stoweidlem59  46074  stoweidlem62  46077  stirlinglem5  46093  fourierdlem31  46153  fourierdlem80  46201  fourierdlem93  46214  sge00  46391  sge0f1o  46397  sge0gerp  46410  sge0pnffigt  46411  sge0lefi  46413  sge0ltfirp  46415  sge0resplit  46421  sge0reuz  46462  iunhoiioolem  46690  smfpimcc  46823  smfsup  46829  smfsupxr  46831  smfinf  46833  smflimsup  46843  nfafv2  47230