Theorem nfrn 5951

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 5687	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5878	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5950	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2901	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2883  ^◡ccnv 5675  dom cdm 5676  ran crn 5677

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-cnv 5684  df-dm 5686  df-rn 5687

This theorem is referenced by:  nfima  6067  nff  6713  nffo  6804  fliftfun  7308  zfrep6  7940  ptbasfi  23084  utopsnneiplem  23751  restmetu  24078  itg2cnlem1  25278  acunirnmpt2  31880  acunirnmpt2f  31881  fnpreimac  31891  fsumiunle  32030  nsgqusf1olem1  32519  nsgqusf1olem3  32521  locfinreflem  32815  prodindf  33016  esumrnmpt2  33061  esumgect  33083  esum2d  33086  esumiun  33087  sigapildsys  33155  ldgenpisyslem1  33156  oms0  33291  breprexplema  33637  bnj1366  33835  exrecfnlem  36255  totbndbnd  36652  refsumcn  43704  disjrnmpt2  43876  disjf1o  43879  disjinfi  43881  choicefi  43889  rnmptbd2lem  43942  infnsuprnmpt  43944  rnmptbdlem  43949  rnmptss2  43951  rnmptssbi  43955  supxrleubrnmpt  44106  suprleubrnmpt  44122  infrnmptle  44123  infxrunb3rnmpt  44128  uzub  44131  supminfrnmpt  44145  infxrgelbrnmpt  44154  infrpgernmpt  44165  supminfxrrnmpt  44171  limsupubuz  44419  liminflelimsuplem  44481  stoweidlem27  44733  stoweidlem29  44735  stoweidlem31  44737  stoweidlem35  44741  stoweidlem59  44765  stoweidlem62  44768  stirlinglem5  44784  fourierdlem31  44844  fourierdlem80  44892  fourierdlem93  44905  sge00  45082  sge0f1o  45088  sge0gerp  45101  sge0pnffigt  45102  sge0lefi  45104  sge0ltfirp  45106  sge0resplit  45112  sge0reuz  45153  iunhoiioolem  45381  smfpimcc  45514  smfsup  45520  smfsupxr  45522  smfinf  45524  smflimsup  45534  nfafv2  45916