![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > nfrn | Unicode version |
Description: Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Ref | Expression |
---|---|
nfrn.1 |
Ref | Expression |
---|---|
nfrn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rn 5015 | . 2 | |
2 | nfrn.1 | . . . 4 | |
3 | 2 | nfcnv 5186 | . . 3 |
4 | 3 | nfdm 5249 | . 2 |
5 | 1, 4 | nfcxfr 2617 | 1 |
Colors of variables: wff setvar class |
Syntax hints: F/_ wnfc 2605 `' ccnv 5003
dom cdm 5004 ran crn 5005 |
This theorem is referenced by: nfima 5350 nff 5732 nffo 5799 fliftfun 6210 zfrep6 6768 ptbasfi 20082 utopsnneiplem 20750 restmetu 21090 itg2cnlem1 22168 locfinreflem 27843 oms0 28266 totbndbnd 30285 refsumcn 31405 suprnmpt 31451 stoweidlem27 31809 stoweidlem29 31811 stoweidlem31 31813 stoweidlem35 31817 stoweidlem59 31841 stoweidlem62 31844 stirlinglem5 31860 fourierdlem31 31920 fourierdlem53 31942 fourierdlem80 31969 fourierdlem93 31982 bnj1366 33888 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-rab 2816 df-v 3111 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-nul 3785 df-if 3942 df-sn 4030 df-pr 4032 df-op 4036 df-br 4453 df-opab 4511 df-cnv 5012 df-dm 5014 df-rn 5015 |
Copyright terms: Public domain | W3C validator |