![]() |
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 5650 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | nfres.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
3 | nfres.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
4 | nfcv 2908 | . . . 4 ⊢ Ⅎ𝑥V | |
5 | 3, 4 | nfxp 5671 | . . 3 ⊢ Ⅎ𝑥(𝐵 × V) |
6 | 2, 5 | nfin 4181 | . 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V)) |
7 | 1, 6 | nfcxfr 2906 | 1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2888 Vcvv 3448 ∩ cin 3914 × cxp 5636 ↾ cres 5640 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-rab 3411 df-in 3922 df-opab 5173 df-xp 5644 df-res 5650 |
This theorem is referenced by: nfima 6026 nffrecs 8219 nfwrecsOLD 8253 frsucmpt 8389 frsucmptn 8390 nfoi 9457 prdsdsf 23736 prdsxmet 23738 limciun 25274 nosupbnd2 27080 noinfbnd2 27095 2ndresdju 31607 gsumpart 31939 bnj1446 33697 bnj1447 33698 bnj1448 33699 bnj1466 33705 bnj1467 33706 bnj1519 33717 bnj1520 33718 bnj1529 33722 feqresmptf 43528 limcperiod 43943 xlimconst2 44150 cncfiooicclem1 44208 stoweidlem28 44343 nfdfat 45433 setrec2lem2 47213 setrec2 47214 |
Copyright terms: Public domain | W3C validator |