Theorem nfrn 5934

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 5662	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5856	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5933	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2921	1 ⊢ Ⅎ𝑥ran 𝐴

This proof depends on syntax axioms:  Ⅎwnfc 2908  ^◡ccnv 5650  dom cdm 5651  ran crn 5652

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  nfima  6064  nff  6703  nffo  6793  fliftfun  7318  zfrep6OLD  7965  ptbasfi  23893  utopsnneiplem  24559  restmetu  24882  itg2cnlem1  26075  acunirnmpt2  33247  acunirnmpt2f  33248  fnpreimac  33257  fsumiunle  33413  prodindf  33422  nsgqusf1olem1  33957  nsgqusf1olem3  33959  locfinreflem  34465  esumrnmpt2  34693  esumgect  34715  esum2d  34718  esumiun  34719  sigapildsys  34788  ldgenpisyslem1  34789  oms0  34922  breprexplema  35252  bnj1366  35452  exrecfnlem  38282  totbndbnd  38703  modelaxreplem3  45948  refsumcn  46016  disjrnmpt2  46172  disjf1o  46175  disjinfi  46176  choicefi  46183  rnmptbd2lem  46229  infnsuprnmpt  46231  rnmptbdlem  46236  rnmptss2  46238  rnmptssbi  46241  supxrleubrnmpt  46385  suprleubrnmpt  46401  infrnmptle  46402  infxrunb3rnmpt  46407  uzub  46410  supminfrnmpt  46424  infxrgelbrnmpt  46433  infrpgernmpt  46444  supminfxrrnmpt  46450  limsupubuz  46692  liminflelimsuplem  46754  stoweidlem27  47006  stoweidlem29  47008  stoweidlem31  47010  stoweidlem35  47014  stoweidlem59  47038  stoweidlem62  47041  stirlinglem5  47057  fourierdlem31  47117  fourierdlem80  47165  fourierdlem93  47178  sge00  47355  sge0f1o  47361  sge0gerp  47374  sge0pnffigt  47375  sge0lefi  47377  sge0ltfirp  47379  sge0resplit  47385  sge0reuz  47426  iunhoiioolem  47654  smfpimcc  47787  smfsup  47793  smfsupxr  47795  smfinf  47797  smflimsup  47807  nfafv2  48257