![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfal | GIF version |
Description: If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfal.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfal | ⊢ Ⅎ𝑥∀𝑦𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfal.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | nfri 1467 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | 2 | hbal 1421 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) |
4 | 3 | nfi 1406 | 1 ⊢ Ⅎ𝑥∀𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: ∀wal 1297 Ⅎwnf 1404 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-7 1392 ax-gen 1393 ax-4 1455 |
This theorem depends on definitions: df-bi 116 df-nf 1405 |
This theorem is referenced by: nfnf 1524 nfa2 1526 aaan 1534 cbv3 1688 cbv2 1693 nfald 1701 cbval2 1856 nfsb4t 1950 nfeuv 1978 mo23 2001 bm1.1 2085 nfnfc1 2243 nfnfc 2247 nfeq 2248 sbcnestgf 3001 dfnfc2 3701 nfdisjv 3864 nfdisj1 3865 nffr 4209 exmidfodomrlemr 6967 exmidfodomrlemrALT 6968 exmidunben 11731 bdsepnft 12666 bdsepnfALT 12668 setindft 12748 strcollnft 12767 strcollnfALT 12769 |
Copyright terms: Public domain | W3C validator |