Theorem nfrn 5933

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 5661	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5855	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5932	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2920	1 ⊢ Ⅎ𝑥ran 𝐴

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  nfima  6063  nff  6705  nffo  6795  fliftfun  7320  zfrep6OLD  7967  ptbasfi  23901  utopsnneiplem  24567  restmetu  24890  itg2cnlem1  26083  acunirnmpt2  33297  acunirnmpt2f  33298  fnpreimac  33307  fsumiunle  33463  prodindf  33472  nsgqusf1olem1  34007  nsgqusf1olem3  34009  locfinreflem  34515  esumrnmpt2  34743  esumgect  34765  esum2d  34768  esumiun  34769  sigapildsys  34838  ldgenpisyslem1  34839  oms0  34972  breprexplema  35302  bnj1366  35502  exrecfnlem  38378  totbndbnd  38799  modelaxreplem3  46046  refsumcn  46123  disjrnmpt2  46279  disjf1o  46282  disjinfi  46283  choicefi  46290  rnmptbd2lem  46336  infnsuprnmpt  46338  rnmptbdlem  46343  rnmptss2  46345  rnmptssbi  46348  supxrleubrnmpt  46492  suprleubrnmpt  46508  infrnmptle  46509  infxrunb3rnmpt  46514  uzub  46517  supminfrnmpt  46531  infxrgelbrnmpt  46540  infrpgernmpt  46551  supminfxrrnmpt  46557  limsupubuz  46799  liminflelimsuplem  46861  stoweidlem27  47113  stoweidlem29  47115  stoweidlem31  47117  stoweidlem35  47121  stoweidlem59  47145  stoweidlem62  47148  stirlinglem5  47164  fourierdlem31  47224  fourierdlem80  47272  fourierdlem93  47285  sge00  47462  sge0f1o  47468  sge0gerp  47481  sge0pnffigt  47482  sge0lefi  47484  sge0ltfirp  47486  sge0resplit  47492  sge0reuz  47533  iunhoiioolem  47761  smfpimcc  47894  smfsup  47900  smfsupxr  47902  smfinf  47904  smflimsup  47914  nfafv2  48364