Theorem nfrn 5891

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 5625	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5817	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5890	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2892	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2879  ^◡ccnv 5613  dom cdm 5614  ran crn 5615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-cnv 5622  df-dm 5624  df-rn 5625

This theorem is referenced by:  nfima  6016  nff  6647  nffo  6734  fliftfun  7246  zfrep6  7887  ptbasfi  23496  utopsnneiplem  24162  restmetu  24485  itg2cnlem1  25689  acunirnmpt2  32642  acunirnmpt2f  32643  fnpreimac  32653  fsumiunle  32812  prodindf  32844  nsgqusf1olem1  33378  nsgqusf1olem3  33380  locfinreflem  33853  esumrnmpt2  34081  esumgect  34103  esum2d  34106  esumiun  34107  sigapildsys  34175  ldgenpisyslem1  34176  oms0  34310  breprexplema  34643  bnj1366  34841  exrecfnlem  37421  totbndbnd  37837  modelaxreplem3  45021  refsumcn  45075  disjrnmpt2  45233  disjf1o  45236  disjinfi  45237  choicefi  45245  rnmptbd2lem  45293  infnsuprnmpt  45295  rnmptbdlem  45300  rnmptss2  45302  rnmptssbi  45305  supxrleubrnmpt  45452  suprleubrnmpt  45468  infrnmptle  45469  infxrunb3rnmpt  45474  uzub  45477  supminfrnmpt  45491  infxrgelbrnmpt  45500  infrpgernmpt  45511  supminfxrrnmpt  45517  limsupubuz  45759  liminflelimsuplem  45821  stoweidlem27  46073  stoweidlem29  46075  stoweidlem31  46077  stoweidlem35  46081  stoweidlem59  46105  stoweidlem62  46108  stirlinglem5  46124  fourierdlem31  46184  fourierdlem80  46232  fourierdlem93  46245  sge00  46422  sge0f1o  46428  sge0gerp  46441  sge0pnffigt  46442  sge0lefi  46444  sge0ltfirp  46446  sge0resplit  46452  sge0reuz  46493  iunhoiioolem  46721  smfpimcc  46854  smfsup  46860  smfsupxr  46862  smfinf  46864  smflimsup  46874  nfafv2  47257