Theorem nfrn 5942

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 5672	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5864	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5941	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2923	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2910  ^◡ccnv 5660  dom cdm 5661  ran crn 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  nfima  6070  nff  6701  nffo  6791  fliftfun  7310  zfrep6OLD  7948  ptbasfi  23738  utopsnneiplem  24404  restmetu  24727  itg2cnlem1  25920  acunirnmpt2  33005  acunirnmpt2f  33006  fnpreimac  33015  fsumiunle  33173  prodindf  33182  nsgqusf1olem1  33722  nsgqusf1olem3  33724  locfinreflem  34230  esumrnmpt2  34458  esumgect  34480  esum2d  34483  esumiun  34484  sigapildsys  34552  ldgenpisyslem1  34553  oms0  34687  breprexplema  35017  bnj1366  35217  exrecfnlem  38025  totbndbnd  38440  modelaxreplem3  45689  refsumcn  45750  disjrnmpt2  45906  disjf1o  45909  disjinfi  45910  choicefi  45917  rnmptbd2lem  45963  infnsuprnmpt  45965  rnmptbdlem  45970  rnmptss2  45972  rnmptssbi  45975  supxrleubrnmpt  46120  suprleubrnmpt  46136  infrnmptle  46137  infxrunb3rnmpt  46142  uzub  46145  supminfrnmpt  46159  infxrgelbrnmpt  46168  infrpgernmpt  46179  supminfxrrnmpt  46185  limsupubuz  46427  liminflelimsuplem  46489  stoweidlem27  46741  stoweidlem29  46743  stoweidlem31  46745  stoweidlem35  46749  stoweidlem59  46773  stoweidlem62  46776  stirlinglem5  46792  fourierdlem31  46852  fourierdlem80  46900  fourierdlem93  46913  sge00  47090  sge0f1o  47096  sge0gerp  47109  sge0pnffigt  47110  sge0lefi  47112  sge0ltfirp  47114  sge0resplit  47120  sge0reuz  47161  iunhoiioolem  47389  smfpimcc  47522  smfsup  47528  smfsupxr  47530  smfinf  47532  smflimsup  47542  nfafv2  47955