![]() |
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 2134 | . 2 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑) | |
2 | nf5i.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
3 | 1, 2 | mpg 1792 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1532 Ⅎwnf 1778 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-10 2130 |
This theorem depends on definitions: df-bi 206 df-ex 1775 df-nf 1779 |
This theorem is referenced by: nfnaew 2138 nfnaewOLD 2139 nfe1 2140 sbh 2260 nf5di 2275 19.9h 2276 19.21h 2277 19.23h 2278 exlimih 2279 exlimdh 2280 equsalhw 2281 equsexhv 2282 hban 2290 hb3an 2291 nfal 2312 hbex 2314 nfsbv 2319 cbv3hv 2331 dvelimhw 2336 cbv3h 2398 equsalh 2414 equsexh 2415 nfae 2427 axc16i 2430 dvelimh 2444 nfs1 2482 hbsb 2518 sb7h 2520 nfsab 2716 nfsabg 2717 cleqh 2856 nfcii 2880 nfralw 3299 bnj596 34602 bnj1146 34647 bnj1379 34686 bnj1464 34700 bnj1468 34702 bnj605 34763 bnj607 34772 bnj916 34789 bnj964 34799 bnj981 34806 bnj983 34807 bnj1014 34817 bnj1123 34842 bnj1373 34886 bnj1417 34897 bnj1445 34900 bnj1463 34911 bnj1497 34916 bj-cbv3hv2 36511 bj-equsalhv 36522 bj-nfs1v 36529 bj-nfsab1 36532 bj-gabima 36657 wl-nfalv 37231 nfequid-o 38619 nfa1-o 38624 2sb5ndVD 44621 2sb5ndALT 44643 |
Copyright terms: Public domain | W3C validator |