MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrn Structured version   Unicode version

Theorem nfrn 5243
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  |-  F/_ x A
Assertion
Ref Expression
nfrn  |-  F/_ x ran  A

Proof of Theorem nfrn
StepHypRef Expression
1 df-rn 5010 . 2  |-  ran  A  =  dom  `' A
2 nfrn.1 . . . 4  |-  F/_ x A
32nfcnv 5179 . . 3  |-  F/_ x `' A
43nfdm 5242 . 2  |-  F/_ x dom  `' A
51, 4nfcxfr 2627 1  |-  F/_ x ran  A
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2615   `'ccnv 4998   dom cdm 4999   ran crn 5000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-cnv 5007  df-dm 5009  df-rn 5010
This theorem is referenced by:  nfima  5343  nff  5725  nffo  5792  fliftfun  6196  zfrep6  6749  ptbasfi  19814  utopsnneiplem  20482  restmetu  20822  itg2cnlem1  21900  oms0  27903  totbndbnd  29886  refsumcn  30983  suprnmpt  31029  stoweidlem27  31327  stoweidlem29  31329  stoweidlem31  31331  stoweidlem35  31335  stoweidlem59  31359  stoweidlem62  31362  stirlinglem5  31378  fourierdlem31  31438  fourierdlem53  31460  fourierdlem80  31487  fourierdlem93  31500  bnj1366  32967
  Copyright terms: Public domain W3C validator