![]() |
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 5700 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | nfres.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
3 | nfres.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
4 | nfcv 2902 | . . . 4 ⊢ Ⅎ𝑥V | |
5 | 3, 4 | nfxp 5721 | . . 3 ⊢ Ⅎ𝑥(𝐵 × V) |
6 | 2, 5 | nfin 4231 | . 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V)) |
7 | 1, 6 | nfcxfr 2900 | 1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2887 Vcvv 3477 ∩ cin 3961 × cxp 5686 ↾ cres 5690 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1539 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-v 3479 df-in 3969 df-opab 5210 df-xp 5694 df-res 5700 |
This theorem is referenced by: nfima 6087 nffrecs 8306 nfwrecsOLD 8340 frsucmpt 8476 frsucmptn 8477 nfoi 9551 prdsdsf 24392 prdsxmet 24394 limciun 25943 nosupbnd2 27775 noinfbnd2 27790 2ndresdju 32665 gsumpart 33042 bnj1446 35037 bnj1447 35038 bnj1448 35039 bnj1466 35045 bnj1467 35046 bnj1519 35057 bnj1520 35058 bnj1529 35062 feqresmptf 45173 limcperiod 45583 xlimconst2 45790 cncfiooicclem1 45848 stoweidlem28 45983 nfdfat 47076 setrec2lem2 48924 setrec2 48925 |
Copyright terms: Public domain | W3C validator |