| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nf5i | Structured version Visualization version GIF version | ||
| Description: Deduce that 𝑥 is not free in 𝜑 from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
| Ref | Expression |
|---|---|
| nf5i.1 | ⊢ (𝜑 → ∀𝑥𝜑) |
| Ref | Expression |
|---|---|
| nf5i | ⊢ Ⅎ𝑥𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nf5-1 2145 | . 2 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑) | |
| 2 | nf5i.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
| 3 | 1, 2 | mpg 1797 | 1 ⊢ Ⅎ𝑥𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-10 2141 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: nfnaew 2149 nfe1 2150 sbh 2273 nf5di 2285 19.9h 2286 19.21h 2287 19.23h 2288 exlimih 2289 exlimdh 2290 equsalhw 2291 equsexhv 2292 hban 2300 hb3an 2301 nfal 2323 hbex 2325 nfsbv 2330 cbv3hv 2342 dvelimhw 2347 cbv3h 2409 equsalh 2425 equsexh 2426 nfae 2438 axc16i 2441 dvelimh 2455 nfs1 2493 hbsb 2529 sb7h 2531 nfsab 2727 nfsabg 2728 cleqh 2871 nfcii 2894 nfralw 3311 bnj596 34760 bnj1146 34805 bnj1379 34844 bnj1464 34858 bnj1468 34860 bnj605 34921 bnj607 34930 bnj916 34947 bnj964 34957 bnj981 34964 bnj983 34965 bnj1014 34975 bnj1123 35000 bnj1373 35044 bnj1417 35055 bnj1445 35058 bnj1463 35069 bnj1497 35074 bj-cbv3hv2 36796 bj-equsalhv 36807 bj-nfs1v 36814 bj-nfsab1 36817 bj-gabima 36941 wl-nfalv 37526 nfequid-o 38911 nfa1-o 38916 2sb5ndVD 44930 2sb5ndALT 44952 |
| Copyright terms: Public domain | W3C validator |