Theorem nfrn 5930

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

Syntax hints:  Ⅎwnfc 2882  ^◡ccnv 5651  dom cdm 5652  ran crn 5653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-br 5118  df-opab 5180  df-cnv 5660  df-dm 5662  df-rn 5663

This theorem is referenced by:  nfima  6053  nff  6699  nffo  6786  fliftfun  7301  zfrep6  7948  ptbasfi  23506  utopsnneiplem  24173  restmetu  24496  itg2cnlem1  25701  acunirnmpt2  32572  acunirnmpt2f  32573  fnpreimac  32583  fsumiunle  32745  prodindf  32777  nsgqusf1olem1  33365  nsgqusf1olem3  33367  locfinreflem  33800  esumrnmpt2  34028  esumgect  34050  esum2d  34053  esumiun  34054  sigapildsys  34122  ldgenpisyslem1  34123  oms0  34258  breprexplema  34591  bnj1366  34789  exrecfnlem  37326  totbndbnd  37742  modelaxreplem3  44939  refsumcn  44988  disjrnmpt2  45146  disjf1o  45149  disjinfi  45150  choicefi  45158  rnmptbd2lem  45206  infnsuprnmpt  45208  rnmptbdlem  45213  rnmptss2  45215  rnmptssbi  45218  supxrleubrnmpt  45367  suprleubrnmpt  45383  infrnmptle  45384  infxrunb3rnmpt  45389  uzub  45392  supminfrnmpt  45406  infxrgelbrnmpt  45415  infrpgernmpt  45426  supminfxrrnmpt  45432  limsupubuz  45678  liminflelimsuplem  45740  stoweidlem27  45992  stoweidlem29  45994  stoweidlem31  45996  stoweidlem35  46000  stoweidlem59  46024  stoweidlem62  46027  stirlinglem5  46043  fourierdlem31  46103  fourierdlem80  46151  fourierdlem93  46164  sge00  46341  sge0f1o  46347  sge0gerp  46360  sge0pnffigt  46361  sge0lefi  46363  sge0ltfirp  46365  sge0resplit  46371  sge0reuz  46412  iunhoiioolem  46640  smfpimcc  46773  smfsup  46779  smfsupxr  46781  smfinf  46783  smflimsup  46793  nfafv2  47183