Theorem nfrn 5943

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 5673	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5865	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5942	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2929	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2916  ^◡ccnv 5661  dom cdm 5662  ran crn 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-cnv 5670  df-dm 5672  df-rn 5673

This theorem is referenced by:  nfima  6071  nff  6702  nffo  6792  fliftfun  7311  zfrep6OLD  7951  ptbasfi  23706  utopsnneiplem  24372  restmetu  24695  itg2cnlem1  25888  acunirnmpt2  32945  acunirnmpt2f  32946  fnpreimac  32955  fsumiunle  33113  prodindf  33122  nsgqusf1olem1  33665  nsgqusf1olem3  33667  locfinreflem  34174  esumrnmpt2  34402  esumgect  34424  esum2d  34427  esumiun  34428  sigapildsys  34496  ldgenpisyslem1  34497  oms0  34631  breprexplema  34961  bnj1366  35161  exrecfnlem  37912  totbndbnd  38327  modelaxreplem3  45580  refsumcn  45641  disjrnmpt2  45797  disjf1o  45800  disjinfi  45801  choicefi  45808  rnmptbd2lem  45854  infnsuprnmpt  45856  rnmptbdlem  45861  rnmptss2  45863  rnmptssbi  45866  supxrleubrnmpt  46011  suprleubrnmpt  46027  infrnmptle  46028  infxrunb3rnmpt  46033  uzub  46036  supminfrnmpt  46050  infxrgelbrnmpt  46059  infrpgernmpt  46070  supminfxrrnmpt  46076  limsupubuz  46318  liminflelimsuplem  46380  stoweidlem27  46632  stoweidlem29  46634  stoweidlem31  46636  stoweidlem35  46640  stoweidlem59  46664  stoweidlem62  46667  stirlinglem5  46683  fourierdlem31  46743  fourierdlem80  46791  fourierdlem93  46804  sge00  46981  sge0f1o  46987  sge0gerp  47000  sge0pnffigt  47001  sge0lefi  47003  sge0ltfirp  47005  sge0resplit  47011  sge0reuz  47052  iunhoiioolem  47280  smfpimcc  47413  smfsup  47419  smfsupxr  47421  smfinf  47423  smflimsup  47433  nfafv2  47843