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

Theorem nfrn 5096
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 4864 . 2  |-  ran  A  =  dom  `' A
2 nfrn.1 . . . 4  |-  F/_ x A
32nfcnv 5032 . . 3  |-  F/_ x `' A
43nfdm 5095 . 2  |-  F/_ x dom  `' A
51, 4nfcxfr 2578 1  |-  F/_ x ran  A
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2566   `'ccnv 4852   dom cdm 4853   ran crn 4854
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-cnv 4861  df-dm 4863  df-rn 4864
This theorem is referenced by:  nfima  5195  nff  5742  nffo  5809  fliftfun  6220  zfrep6  6775  ptbasfi  20594  utopsnneiplem  21260  restmetu  21583  itg2cnlem1  22717  acunirnmpt2  28264  acunirnmpt2f  28265  locfinreflem  28675  esumrnmpt2  28897  esumgect  28919  esum2d  28922  esumiun  28923  sigapildsys  28992  ldgenpisyslem1  28993  oms0  29133  oms0OLD  29137  bnj1366  29649  totbndbnd  32085  refsumcn  37324  suprnmpt  37399  wessf1ornlem  37420  disjrnmpt2  37424  disjf1o  37427  disjinfi  37429  stoweidlem27  37827  stoweidlem29  37829  stoweidlem29OLD  37830  stoweidlem31  37832  stoweidlem35  37836  stoweidlem59  37860  stoweidlem62  37863  stoweidlem62OLD  37864  stirlinglem5  37880  fourierdlem31  37940  fourierdlem31OLD  37941  fourierdlem53  37963  fourierdlem80  37990  fourierdlem93  38003  sge00  38126  sge0f1o  38132  sge0gerp  38145  sge0pnffigt  38146  sge0lefi  38148  sge0ltfirp  38150  sge0resplit  38156
  Copyright terms: Public domain W3C validator