Theorem nfrn 5537

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 5288	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5469	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5536	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2905	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2894  ^◡ccnv 5276  dom cdm 5277  ran crn 5278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-br 4810  df-opab 4872  df-cnv 5285  df-dm 5287  df-rn 5288

This theorem is referenced by:  nfima  5656  nff  6219  nffo  6297  fliftfun  6754  zfrep6  7332  ptbasfi  21664  utopsnneiplem  22330  restmetu  22654  itg2cnlem1  23819  acunirnmpt2  29845  acunirnmpt2f  29846  fsumiunle  29959  locfinreflem  30289  prodindf  30467  esumrnmpt2  30512  esumgect  30534  esum2d  30537  esumiun  30538  sigapildsys  30607  ldgenpisyslem1  30608  oms0  30741  breprexplema  31091  bnj1366  31280  totbndbnd  33942  refsumcn  39773  suprnmpt  39934  wessf1ornlem  39950  disjrnmpt2  39954  disjf1o  39957  disjinfi  39959  choicefi  39969  rnmptbd2lem  40036  infnsuprnmpt  40038  rnmptbdlem  40043  rnmptss2  40045  rnmptssbi  40050  supxrleubrnmpt  40201  suprleubrnmpt  40218  infrnmptle  40219  infxrunb3rnmpt  40224  uzub  40227  supminfrnmpt  40241  infxrgelbrnmpt  40252  infrpgernmpt  40264  supminfxrrnmpt  40270  limsupubuz  40515  liminflelimsuplem  40577  stoweidlem27  40813  stoweidlem29  40815  stoweidlem31  40817  stoweidlem35  40821  stoweidlem59  40845  stoweidlem62  40848  stirlinglem5  40864  fourierdlem31  40924  fourierdlem53  40945  fourierdlem80  40972  fourierdlem93  40985  sge00  41162  sge0f1o  41168  sge0gerp  41181  sge0pnffigt  41182  sge0lefi  41184  sge0ltfirp  41186  sge0resplit  41192  sge0reuz  41233  iunhoiioolem  41461  smfpimcc  41586  smfsup  41592  smfsupxr  41594  smfinf  41596  smflimsup  41606  nfafv2  41898