Theorem nfrn 5909

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 5643	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5835	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5908	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2897	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2884  ^◡ccnv 5631  dom cdm 5632  ran crn 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  nfima  6035  nff  6666  nffo  6753  fliftfun  7268  zfrep6  7909  ptbasfi  23537  utopsnneiplem  24203  restmetu  24526  itg2cnlem1  25730  acunirnmpt2  32750  acunirnmpt2f  32751  fnpreimac  32760  fsumiunle  32921  prodindf  32955  nsgqusf1olem1  33506  nsgqusf1olem3  33508  locfinreflem  34018  esumrnmpt2  34246  esumgect  34268  esum2d  34271  esumiun  34272  sigapildsys  34340  ldgenpisyslem1  34341  oms0  34475  breprexplema  34808  bnj1366  35005  exrecfnlem  37634  totbndbnd  38040  modelaxreplem3  45336  refsumcn  45390  disjrnmpt2  45547  disjf1o  45550  disjinfi  45551  choicefi  45558  rnmptbd2lem  45606  infnsuprnmpt  45608  rnmptbdlem  45613  rnmptss2  45615  rnmptssbi  45618  supxrleubrnmpt  45764  suprleubrnmpt  45780  infrnmptle  45781  infxrunb3rnmpt  45786  uzub  45789  supminfrnmpt  45803  infxrgelbrnmpt  45812  infrpgernmpt  45823  supminfxrrnmpt  45829  limsupubuz  46071  liminflelimsuplem  46133  stoweidlem27  46385  stoweidlem29  46387  stoweidlem31  46389  stoweidlem35  46393  stoweidlem59  46417  stoweidlem62  46420  stirlinglem5  46436  fourierdlem31  46496  fourierdlem80  46544  fourierdlem93  46557  sge00  46734  sge0f1o  46740  sge0gerp  46753  sge0pnffigt  46754  sge0lefi  46756  sge0ltfirp  46758  sge0resplit  46764  sge0reuz  46805  iunhoiioolem  47033  smfpimcc  47166  smfsup  47172  smfsupxr  47174  smfinf  47176  smflimsup  47186  nfafv2  47578