New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > nfi | GIF version |
Description: Deduce that x is not free in φ from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfi.1 | ⊢ (φ → ∀xφ) |
Ref | Expression |
---|---|
nfi | ⊢ Ⅎxφ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nf 1545 | . 2 ⊢ (Ⅎxφ ↔ ∀x(φ → ∀xφ)) | |
2 | nfi.1 | . 2 ⊢ (φ → ∀xφ) | |
3 | 1, 2 | mpgbir 1550 | 1 ⊢ Ⅎxφ |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 Ⅎwnf 1544 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 |
This theorem depends on definitions: df-bi 177 df-nf 1545 |
This theorem is referenced by: nfth 1553 nfnth 1556 nfv 1619 nfe1 1732 nfdh 1767 19.9h 1780 nfa1 1788 19.21h 1797 19.23h 1802 exlimih 1804 exlimdh 1807 nfim1 1811 nfim1OLD 1812 hban 1828 hb3an 1830 nfal 1842 nfex 1843 nfan1 1881 nfae 1954 equsalh 1961 equsexh 1963 sbh 2027 nfs1 2044 ax16i 2046 nfs1v 2106 hbsb 2110 sb7h 2121 nfequid-o 2161 nfa1-o 2166 nfsab1 2343 nfsab 2345 nfcii 2480 nfcri 2483 |
Copyright terms: Public domain | W3C validator |