Theorem nfrn 5821

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 5562	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5747	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5820	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2902	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2884  ^◡ccnv 5550  dom cdm 5551  ran crn 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-cnv 5559  df-dm 5561  df-rn 5562

This theorem is referenced by:  nfima  5937  nff  6541  nffo  6632  fliftfun  7121  zfrep6  7728  ptbasfi  22478  utopsnneiplem  23145  restmetu  23468  itg2cnlem1  24659  acunirnmpt2  30717  acunirnmpt2f  30718  fnpreimac  30728  fsumiunle  30863  nsgqusf1olem1  31312  nsgqusf1olem3  31314  locfinreflem  31504  prodindf  31703  esumrnmpt2  31748  esumgect  31770  esum2d  31773  esumiun  31774  sigapildsys  31842  ldgenpisyslem1  31843  oms0  31976  breprexplema  32322  bnj1366  32522  exrecfnlem  35287  totbndbnd  35684  refsumcn  42246  disjrnmpt2  42399  disjf1o  42402  disjinfi  42404  choicefi  42413  rnmptbd2lem  42466  infnsuprnmpt  42468  rnmptbdlem  42473  rnmptss2  42475  rnmptssbi  42479  supxrleubrnmpt  42619  suprleubrnmpt  42635  infrnmptle  42636  infxrunb3rnmpt  42641  uzub  42644  supminfrnmpt  42658  infxrgelbrnmpt  42669  infrpgernmpt  42680  supminfxrrnmpt  42686  limsupubuz  42929  liminflelimsuplem  42991  stoweidlem27  43243  stoweidlem29  43245  stoweidlem31  43247  stoweidlem35  43251  stoweidlem59  43275  stoweidlem62  43278  stirlinglem5  43294  fourierdlem31  43354  fourierdlem80  43402  fourierdlem93  43415  sge00  43589  sge0f1o  43595  sge0gerp  43608  sge0pnffigt  43609  sge0lefi  43611  sge0ltfirp  43613  sge0resplit  43619  sge0reuz  43660  iunhoiioolem  43888  smfpimcc  44013  smfsup  44019  smfsupxr  44021  smfinf  44023  smflimsup  44033  nfafv2  44382