Theorem nfrn 5894

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

Syntax hints:  Ⅎwnfc 2876  ^◡ccnv 5618  dom cdm 5619  ran crn 5620

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  nfima  6019  nff  6648  nffo  6735  fliftfun  7249  zfrep6  7890  ptbasfi  23466  utopsnneiplem  24133  restmetu  24456  itg2cnlem1  25660  acunirnmpt2  32603  acunirnmpt2f  32604  fnpreimac  32614  fsumiunle  32774  prodindf  32806  nsgqusf1olem1  33350  nsgqusf1olem3  33352  locfinreflem  33807  esumrnmpt2  34035  esumgect  34057  esum2d  34060  esumiun  34061  sigapildsys  34129  ldgenpisyslem1  34130  oms0  34265  breprexplema  34598  bnj1366  34796  exrecfnlem  37353  totbndbnd  37769  modelaxreplem3  44954  refsumcn  45008  disjrnmpt2  45166  disjf1o  45169  disjinfi  45170  choicefi  45178  rnmptbd2lem  45226  infnsuprnmpt  45228  rnmptbdlem  45233  rnmptss2  45235  rnmptssbi  45238  supxrleubrnmpt  45385  suprleubrnmpt  45401  infrnmptle  45402  infxrunb3rnmpt  45407  uzub  45410  supminfrnmpt  45424  infxrgelbrnmpt  45433  infrpgernmpt  45444  supminfxrrnmpt  45450  limsupubuz  45694  liminflelimsuplem  45756  stoweidlem27  46008  stoweidlem29  46010  stoweidlem31  46012  stoweidlem35  46016  stoweidlem59  46040  stoweidlem62  46043  stirlinglem5  46059  fourierdlem31  46119  fourierdlem80  46167  fourierdlem93  46180  sge00  46357  sge0f1o  46363  sge0gerp  46376  sge0pnffigt  46377  sge0lefi  46379  sge0ltfirp  46381  sge0resplit  46387  sge0reuz  46428  iunhoiioolem  46656  smfpimcc  46789  smfsup  46795  smfsupxr  46797  smfinf  46799  smflimsup  46809  nfafv2  47202