Theorem nfrn 5928

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 5658	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5850	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5927	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2922	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2909  ^◡ccnv 5646  dom cdm 5647  ran crn 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5655  df-dm 5657  df-rn 5658

This theorem is referenced by:  nfima  6057  nff  6687  nffo  6777  fliftfun  7296  zfrep6OLD  7936  ptbasfi  23638  utopsnneiplem  24304  restmetu  24627  itg2cnlem1  25820  acunirnmpt2  32859  acunirnmpt2f  32860  fnpreimac  32869  fsumiunle  33028  prodindf  33037  nsgqusf1olem1  33596  nsgqusf1olem3  33598  locfinreflem  34134  esumrnmpt2  34362  esumgect  34384  esum2d  34387  esumiun  34388  sigapildsys  34456  ldgenpisyslem1  34457  oms0  34591  breprexplema  34921  bnj1366  35121  exrecfnlem  37870  totbndbnd  38285  modelaxreplem3  45553  refsumcn  45607  disjrnmpt2  45763  disjf1o  45766  disjinfi  45767  choicefi  45774  rnmptbd2lem  45820  infnsuprnmpt  45822  rnmptbdlem  45827  rnmptss2  45829  rnmptssbi  45832  supxrleubrnmpt  45977  suprleubrnmpt  45993  infrnmptle  45994  infxrunb3rnmpt  45999  uzub  46002  supminfrnmpt  46016  infxrgelbrnmpt  46025  infrpgernmpt  46036  supminfxrrnmpt  46042  limsupubuz  46284  liminflelimsuplem  46346  stoweidlem27  46598  stoweidlem29  46600  stoweidlem31  46602  stoweidlem35  46606  stoweidlem59  46630  stoweidlem62  46633  stirlinglem5  46649  fourierdlem31  46709  fourierdlem80  46757  fourierdlem93  46770  sge00  46947  sge0f1o  46953  sge0gerp  46966  sge0pnffigt  46967  sge0lefi  46969  sge0ltfirp  46971  sge0resplit  46977  sge0reuz  47018  iunhoiioolem  47246  smfpimcc  47379  smfsup  47385  smfsupxr  47387  smfinf  47389  smflimsup  47399  nfafv2  47809