Theorem nfrn 5946

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 5669	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5868	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5945	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2924	1 ⊢ Ⅎ𝑥ran 𝐴

This proof depends on syntax axioms:  Ⅎwnfc 2911  ^◡ccnv 5657  dom cdm 5658  ran crn 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-cnv 5666  df-dm 5668  df-rn 5669

This theorem is used by:  nfima  6082  nff  6735  nffo  6825  fliftfun  7351  zfrep6OLD  8001  ptbasfi  23955  utopsnneiplem  24621  restmetu  24944  itg2cnlem1  26137  acunirnmpt2  33352  acunirnmpt2f  33353  fnpreimac  33362  fsumiunle  33516  prodindf  33525  nsgqusf1olem1  34068  nsgqusf1olem3  34070  locfinreflem  34583  esumrnmpt2  34811  esumgect  34833  esum2d  34836  esumiun  34837  sigapildsys  34906  ldgenpisyslem1  34907  oms0  35040  breprexplema  35370  bnj1366  35570  exrecfnlem  38570  totbndbnd  38989  modelaxreplem3  46234  refsumcn  46321  disjrnmpt2  46476  disjf1o  46479  disjinfi  46480  choicefi  46487  rnmptbd2lem  46533  infnsuprnmpt  46535  rnmptbdlem  46540  rnmptss2  46542  rnmptssbi  46545  supxrleubrnmpt  46689  suprleubrnmpt  46705  infrnmptle  46706  infxrunb3rnmpt  46711  uzub  46714  supminfrnmpt  46728  infxrgelbrnmpt  46737  infrpgernmpt  46748  supminfxrrnmpt  46754  limsupubuz  46996  liminflelimsuplem  47058  stoweidlem27  47310  stoweidlem29  47312  stoweidlem31  47314  stoweidlem35  47318  stoweidlem59  47342  stoweidlem62  47345  stirlinglem5  47361  fourierdlem31  47421  fourierdlem80  47469  fourierdlem93  47482  sge00  47659  sge0f1o  47665  sge0gerp  47678  sge0pnffigt  47679  sge0lefi  47681  sge0ltfirp  47683  sge0resplit  47689  sge0reuz  47730  iunhoiioolem  47958  smfpimcc  48091  smfsup  48097  smfsupxr  48099  smfinf  48101  smflimsup  48111  nfafv2  48561