Theorem nfrn 5916

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

Syntax hints:  Ⅎwnfc 2876  ^◡ccnv 5637  dom cdm 5638  ran crn 5639

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  nfima  6039  nff  6684  nffo  6771  fliftfun  7287  zfrep6  7933  ptbasfi  23468  utopsnneiplem  24135  restmetu  24458  itg2cnlem1  25662  acunirnmpt2  32584  acunirnmpt2f  32585  fnpreimac  32595  fsumiunle  32754  prodindf  32786  nsgqusf1olem1  33384  nsgqusf1olem3  33386  locfinreflem  33830  esumrnmpt2  34058  esumgect  34080  esum2d  34083  esumiun  34084  sigapildsys  34152  ldgenpisyslem1  34153  oms0  34288  breprexplema  34621  bnj1366  34819  exrecfnlem  37367  totbndbnd  37783  modelaxreplem3  44970  refsumcn  45024  disjrnmpt2  45182  disjf1o  45185  disjinfi  45186  choicefi  45194  rnmptbd2lem  45242  infnsuprnmpt  45244  rnmptbdlem  45249  rnmptss2  45251  rnmptssbi  45254  supxrleubrnmpt  45402  suprleubrnmpt  45418  infrnmptle  45419  infxrunb3rnmpt  45424  uzub  45427  supminfrnmpt  45441  infxrgelbrnmpt  45450  infrpgernmpt  45461  supminfxrrnmpt  45467  limsupubuz  45711  liminflelimsuplem  45773  stoweidlem27  46025  stoweidlem29  46027  stoweidlem31  46029  stoweidlem35  46033  stoweidlem59  46057  stoweidlem62  46060  stirlinglem5  46076  fourierdlem31  46136  fourierdlem80  46184  fourierdlem93  46197  sge00  46374  sge0f1o  46380  sge0gerp  46393  sge0pnffigt  46394  sge0lefi  46396  sge0ltfirp  46398  sge0resplit  46404  sge0reuz  46445  iunhoiioolem  46673  smfpimcc  46806  smfsup  46812  smfsupxr  46814  smfinf  46816  smflimsup  46826  nfafv2  47219