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 2140 | . 2 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑) | |
2 | nf5i.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
3 | 1, 2 | mpg 1789 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-10 2136 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-nf 1776 |
This theorem is referenced by: nfnaew 2144 nfe1 2145 sbh 2264 nf5di 2285 19.9h 2286 19.21h 2287 19.23h 2288 exlimih 2289 exlimdh 2290 equsalhw 2291 equsexhv 2292 hban 2300 hb3an 2301 nfal 2334 hbex 2336 hbsbw 2343 cbv3hv 2352 dvelimhw 2358 cbv3h 2418 equsalh 2436 equsexh 2437 nfae 2450 axc16i 2453 dvelimh 2467 nfs1 2523 hbsb 2563 sb7h 2565 nfsab1OLD 2809 nfsab 2812 nfsabg 2813 cleqh 2936 nfcii 2965 nfcri 2971 bnj596 31917 bnj1146 31963 bnj1379 32002 bnj1464 32016 bnj1468 32018 bnj605 32079 bnj607 32088 bnj916 32105 bnj964 32115 bnj981 32122 bnj983 32123 bnj1014 32132 bnj1123 32156 bnj1373 32200 bnj1417 32211 bnj1445 32214 bnj1463 32225 bnj1497 32230 bj-cbv3hv2 34015 bj-equsalhv 34026 bj-nfs1v 34033 bj-nfsab1 34036 wl-nfalv 34648 nfequid-o 35928 nfa1-o 35933 2sb5ndVD 41124 2sb5ndALT 41146 |
Copyright terms: Public domain | W3C validator |