![]() |
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 5529 | . 2 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | nfres.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
3 | nfres.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
4 | nfcv 2917 | . . . 4 ⊢ Ⅎ𝑥V | |
5 | 3, 4 | nfxp 5550 | . . 3 ⊢ Ⅎ𝑥(𝐵 × V) |
6 | 2, 5 | nfin 4117 | . 2 ⊢ Ⅎ𝑥(𝐴 ∩ (𝐵 × V)) |
7 | 1, 6 | nfcxfr 2915 | 1 ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2897 Vcvv 3407 ∩ cin 3853 × cxp 5515 ↾ cres 5519 |
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 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-rab 3077 df-in 3861 df-opab 5088 df-xp 5523 df-res 5529 |
This theorem is referenced by: nfima 5902 nfwrecs 7952 frsucmpt 8076 frsucmptn 8077 nfoi 8996 prdsdsf 23054 prdsxmet 23056 limciun 24578 2ndresdju 30494 gsumpart 30826 bnj1446 32530 bnj1447 32531 bnj1448 32532 bnj1466 32538 bnj1467 32539 bnj1519 32550 bnj1520 32551 bnj1529 32555 trpredlem1 33298 trpredrec 33309 nffrecs 33366 nosupbnd2 33469 noinfbnd2 33484 feqresmptf 42218 limcperiod 42621 xlimconst2 42828 cncfiooicclem1 42886 stoweidlem28 43021 nfdfat 44036 setrec2lem2 45574 setrec2 45575 |
Copyright terms: Public domain | W3C validator |