Theorem nfrn 5905

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 5642	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5832	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5904	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2889	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2876  ^◡ccnv 5630  dom cdm 5631  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  nfima  6028  nff  6666  nffo  6753  fliftfun  7269  zfrep6  7913  ptbasfi  23501  utopsnneiplem  24168  restmetu  24491  itg2cnlem1  25695  acunirnmpt2  32634  acunirnmpt2f  32635  fnpreimac  32645  fsumiunle  32804  prodindf  32836  nsgqusf1olem1  33377  nsgqusf1olem3  33379  locfinreflem  33823  esumrnmpt2  34051  esumgect  34073  esum2d  34076  esumiun  34077  sigapildsys  34145  ldgenpisyslem1  34146  oms0  34281  breprexplema  34614  bnj1366  34812  exrecfnlem  37360  totbndbnd  37776  modelaxreplem3  44963  refsumcn  45017  disjrnmpt2  45175  disjf1o  45178  disjinfi  45179  choicefi  45187  rnmptbd2lem  45235  infnsuprnmpt  45237  rnmptbdlem  45242  rnmptss2  45244  rnmptssbi  45247  supxrleubrnmpt  45395  suprleubrnmpt  45411  infrnmptle  45412  infxrunb3rnmpt  45417  uzub  45420  supminfrnmpt  45434  infxrgelbrnmpt  45443  infrpgernmpt  45454  supminfxrrnmpt  45460  limsupubuz  45704  liminflelimsuplem  45766  stoweidlem27  46018  stoweidlem29  46020  stoweidlem31  46022  stoweidlem35  46026  stoweidlem59  46050  stoweidlem62  46053  stirlinglem5  46069  fourierdlem31  46129  fourierdlem80  46177  fourierdlem93  46190  sge00  46367  sge0f1o  46373  sge0gerp  46386  sge0pnffigt  46387  sge0lefi  46389  sge0ltfirp  46391  sge0resplit  46397  sge0reuz  46438  iunhoiioolem  46666  smfpimcc  46799  smfsup  46805  smfsupxr  46807  smfinf  46809  smflimsup  46819  nfafv2  47212