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

Theorem nfrn 4958
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 4737 . 2  |-  ran  A  =  dom  `' A
2 nfrn.1 . . . 4  |-  F/_ x A
32nfcnv 4897 . . 3  |-  F/_ x `' A
43nfdm 4957 . 2  |-  F/_ x dom  `' A
51, 4nfcxfr 2449 1  |-  F/_ x ran  A
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2439   `'ccnv 4725   dom cdm 4726   ran crn 4727
This theorem is referenced by:  nfima  5057  nff  5425  nffo  5488  zfrep6  5789  fliftfun  5853  ptbasfi  17332  itg2cnlem1  19169  restmetu  23513  totbndbnd  25661  refsumcn  26849  stoweidlem27  26924  stoweidlem29  26926  stoweidlem31  26928  stoweidlem35  26932  stoweidlem59  26956  stoweidlem62  26959  stirlinglem5  26975  bnj1366  28373
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-br 4061  df-opab 4115  df-cnv 4734  df-dm 4736  df-rn 4737
  Copyright terms: Public domain W3C validator