New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > nfal | GIF version |
Description: If x is not free in φ, it is not free in ∀yφ. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfal.1 | ⊢ Ⅎxφ |
Ref | Expression |
---|---|
nfal | ⊢ Ⅎx∀yφ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfal.1 | . . . 4 ⊢ Ⅎxφ | |
2 | 1 | nfri 1762 | . . 3 ⊢ (φ → ∀xφ) |
3 | 2 | hbal 1736 | . 2 ⊢ (∀yφ → ∀x∀yφ) |
4 | 3 | nfi 1551 | 1 ⊢ Ⅎx∀yφ |
Colors of variables: wff setvar class |
Syntax hints: ∀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 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-7 1734 ax-11 1746 |
This theorem depends on definitions: df-bi 177 df-ex 1542 df-nf 1545 |
This theorem is referenced by: nfexOLD 1844 nfnf 1845 nfnfOLD 1846 nfald 1852 nfaldOLD 1853 nfa2 1855 aaan 1884 pm11.53 1893 19.12vv 1898 cbval2 2004 sb8 2092 euf 2210 mo 2226 2mo 2282 2eu3 2286 bm1.1 2338 nfnfc1 2492 nfnfc 2495 nfeq 2496 sbcnestgf 3183 dfnfc2 3909 |
Copyright terms: Public domain | W3C validator |