Theorem nfrn 5954

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 5689	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5881	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5953	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2889	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2875  ^◡ccnv 5677  dom cdm 5678  ran crn 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-cnv 5686  df-dm 5688  df-rn 5689

This theorem is referenced by:  nfima  6072  nff  6719  nffo  6809  fliftfun  7319  zfrep6  7959  ptbasfi  23529  utopsnneiplem  24196  restmetu  24523  itg2cnlem1  25735  acunirnmpt2  32527  acunirnmpt2f  32528  fnpreimac  32538  fsumiunle  32677  nsgqusf1olem1  33225  nsgqusf1olem3  33227  locfinreflem  33572  prodindf  33773  esumrnmpt2  33818  esumgect  33840  esum2d  33843  esumiun  33844  sigapildsys  33912  ldgenpisyslem1  33913  oms0  34048  breprexplema  34393  bnj1366  34591  exrecfnlem  36989  totbndbnd  37393  refsumcn  44534  disjrnmpt2  44700  disjf1o  44703  disjinfi  44704  choicefi  44712  rnmptbd2lem  44762  infnsuprnmpt  44764  rnmptbdlem  44769  rnmptss2  44771  rnmptssbi  44775  supxrleubrnmpt  44926  suprleubrnmpt  44942  infrnmptle  44943  infxrunb3rnmpt  44948  uzub  44951  supminfrnmpt  44965  infxrgelbrnmpt  44974  infrpgernmpt  44985  supminfxrrnmpt  44991  limsupubuz  45239  liminflelimsuplem  45301  stoweidlem27  45553  stoweidlem29  45555  stoweidlem31  45557  stoweidlem35  45561  stoweidlem59  45585  stoweidlem62  45588  stirlinglem5  45604  fourierdlem31  45664  fourierdlem80  45712  fourierdlem93  45725  sge00  45902  sge0f1o  45908  sge0gerp  45921  sge0pnffigt  45922  sge0lefi  45924  sge0ltfirp  45926  sge0resplit  45932  sge0reuz  45973  iunhoiioolem  46201  smfpimcc  46334  smfsup  46340  smfsupxr  46342  smfinf  46344  smflimsup  46354  nfafv2  46736