Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfres | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.) |
Ref | Expression |
---|---|
nfres.1 | ⊢ Ⅎ𝑥𝐴 |
nfres.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfres | ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-res 5126 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | nfres.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
3 | nfres.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
4 | nfcv 2764 | . . . 4 ⊢ Ⅎ𝑥V | |
5 | 3, 4 | nfxp 5142 | . . 3 ⊢ Ⅎ𝑥(𝐵 × V) |
6 | 2, 5 | nfin 3820 | . 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V)) |
7 | 1, 6 | nfcxfr 2762 | 1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2751 Vcvv 3200 ∩ cin 3573 × cxp 5112 ↾ cres 5116 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-in 3581 df-opab 4713 df-xp 5120 df-res 5126 |
This theorem is referenced by: nfima 5474 nfwrecs 7409 frsucmpt 7533 frsucmptn 7534 nfoi 8419 prdsdsf 22172 prdsxmet 22174 limciun 23658 bnj1446 31113 bnj1447 31114 bnj1448 31115 bnj1466 31121 bnj1467 31122 bnj1519 31133 bnj1520 31134 bnj1529 31138 trpredlem1 31727 trpredrec 31738 nosupbnd2 31862 wessf1ornlem 39371 feqresmptf 39433 limcperiod 39860 xlimconst2 40061 cncfiooicclem1 40106 stoweidlem28 40245 nfdfat 41210 setrec2lem2 42441 setrec2 42442 |
Copyright terms: Public domain | W3C validator |