Theorem nfrn 5919

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 5652	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5845	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5918	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2890	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2877  ^◡ccnv 5640  dom cdm 5641  ran crn 5642

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-cnv 5649  df-dm 5651  df-rn 5652

This theorem is referenced by:  nfima  6042  nff  6687  nffo  6774  fliftfun  7290  zfrep6  7936  ptbasfi  23475  utopsnneiplem  24142  restmetu  24465  itg2cnlem1  25669  acunirnmpt2  32591  acunirnmpt2f  32592  fnpreimac  32602  fsumiunle  32761  prodindf  32793  nsgqusf1olem1  33391  nsgqusf1olem3  33393  locfinreflem  33837  esumrnmpt2  34065  esumgect  34087  esum2d  34090  esumiun  34091  sigapildsys  34159  ldgenpisyslem1  34160  oms0  34295  breprexplema  34628  bnj1366  34826  exrecfnlem  37374  totbndbnd  37790  modelaxreplem3  44977  refsumcn  45031  disjrnmpt2  45189  disjf1o  45192  disjinfi  45193  choicefi  45201  rnmptbd2lem  45249  infnsuprnmpt  45251  rnmptbdlem  45256  rnmptss2  45258  rnmptssbi  45261  supxrleubrnmpt  45409  suprleubrnmpt  45425  infrnmptle  45426  infxrunb3rnmpt  45431  uzub  45434  supminfrnmpt  45448  infxrgelbrnmpt  45457  infrpgernmpt  45468  supminfxrrnmpt  45474  limsupubuz  45718  liminflelimsuplem  45780  stoweidlem27  46032  stoweidlem29  46034  stoweidlem31  46036  stoweidlem35  46040  stoweidlem59  46064  stoweidlem62  46067  stirlinglem5  46083  fourierdlem31  46143  fourierdlem80  46191  fourierdlem93  46204  sge00  46381  sge0f1o  46387  sge0gerp  46400  sge0pnffigt  46401  sge0lefi  46403  sge0ltfirp  46405  sge0resplit  46411  sge0reuz  46452  iunhoiioolem  46680  smfpimcc  46813  smfsup  46819  smfsupxr  46821  smfinf  46823  smflimsup  46833  nfafv2  47223