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

Theorem nfrn 5082
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 4851 . 2  |-  ran  A  =  dom  `' A
2 nfrn.1 . . . 4  |-  F/_ x A
32nfcnv 5018 . . 3  |-  F/_ x `' A
43nfdm 5081 . 2  |-  F/_ x dom  `' A
51, 4nfcxfr 2576 1  |-  F/_ x ran  A
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2566   `'ccnv 4839   dom cdm 4840   ran crn 4841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-cnv 4848  df-dm 4850  df-rn 4851
This theorem is referenced by:  nfima  5177  nff  5555  nffo  5619  fliftfun  6005  zfrep6  6545  ptbasfi  19154  utopsnneiplem  19822  restmetu  20162  itg2cnlem1  21239  oms0  26710  totbndbnd  28688  refsumcn  29752  stoweidlem27  29822  stoweidlem29  29824  stoweidlem31  29826  stoweidlem35  29830  stoweidlem59  29854  stoweidlem62  29857  stirlinglem5  29873  bnj1366  31823
  Copyright terms: Public domain W3C validator