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 2143 | . 2 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑) | |
2 | nf5i.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
3 | 1, 2 | mpg 1792 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1529 Ⅎ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 2139 |
This theorem depends on definitions: df-bi 209 df-ex 1775 df-nf 1779 |
This theorem is referenced by: nfnaew 2147 nfe1 2148 sbh 2266 nf5di 2287 19.9h 2288 19.21h 2289 19.23h 2290 exlimih 2291 exlimdh 2292 equsalhw 2293 equsexhv 2294 hban 2302 hb3an 2303 nfal 2336 hbex 2338 hbsbw 2345 cbv3hv 2354 dvelimhw 2360 cbv3h 2418 equsalh 2436 equsexh 2437 nfae 2449 axc16i 2452 dvelimh 2466 nfs1 2521 hbsb 2561 sb7h 2563 nfsab1OLD 2807 nfsab 2810 nfsabg 2811 cleqh 2934 nfcii 2963 nfcri 2969 bnj596 32010 bnj1146 32056 bnj1379 32095 bnj1464 32109 bnj1468 32111 bnj605 32172 bnj607 32181 bnj916 32198 bnj964 32208 bnj981 32215 bnj983 32216 bnj1014 32226 bnj1123 32251 bnj1373 32295 bnj1417 32306 bnj1445 32309 bnj1463 32320 bnj1497 32325 bj-cbv3hv2 34110 bj-equsalhv 34121 bj-nfs1v 34128 bj-nfsab1 34131 wl-nfalv 34757 nfequid-o 36038 nfa1-o 36043 2sb5ndVD 41235 2sb5ndALT 41257 |
Copyright terms: Public domain | W3C validator |