![]() |
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 2083 | . 2 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑) | |
2 | nf5i.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
3 | 1, 2 | mpg 1760 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1505 Ⅎwnf 1746 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-10 2079 |
This theorem depends on definitions: df-bi 199 df-ex 1743 df-nf 1747 |
This theorem is referenced by: nfe1 2087 sbh 2201 nf5di 2219 19.9h 2220 19.21h 2221 19.23h 2222 exlimih 2223 exlimdh 2224 equsalhw 2225 equsexhv 2226 hban 2234 hb3an 2235 nfal 2263 hbex 2265 cbv3hv 2276 dvelimhw 2279 cbv3h 2337 equsalh 2355 equsexh 2356 nfae 2369 axc16i 2372 dvelimh 2386 nfs1 2448 hbsb 2489 sb7h 2492 nfsab1OLD 2768 nfsab 2770 cleqh 2889 nfcii 2920 nfcri 2926 bnj596 31671 bnj1146 31717 bnj1379 31756 bnj1464 31769 bnj1468 31771 bnj605 31832 bnj607 31841 bnj916 31858 bnj964 31868 bnj981 31875 bnj983 31876 bnj1014 31885 bnj1123 31909 bnj1373 31953 bnj1417 31964 bnj1445 31967 bnj1463 31978 bnj1497 31983 bj-cbv3hv2 33581 bj-equsalhv 33595 bj-nfs1v 33605 bj-nfsab1 33610 wl-nfalv 34214 nfequid-o 35497 nfa1-o 35502 2sb5ndVD 40669 2sb5ndALT 40691 |
Copyright terms: Public domain | W3C validator |