![]() |
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.) Remove dependency on ax-4 1520. (Revised by Gino Giotto, 25-Aug-2024.) |
Ref | Expression |
---|---|
nfal.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfal | ⊢ Ⅎ𝑥∀𝑦𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nf 1471 | . . . . . 6 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) | |
2 | 1 | biimpi 120 | . . . . 5 ⊢ (Ⅎ𝑥𝜑 → ∀𝑥(𝜑 → ∀𝑥𝜑)) |
3 | 2 | alimi 1465 | . . . 4 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑)) |
4 | ax-7 1458 | . . . 4 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)) | |
5 | ax-5 1457 | . . . . . 6 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)) | |
6 | ax-7 1458 | . . . . . 6 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
7 | 5, 6 | syl6 33 | . . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
8 | 7 | alimi 1465 | . . . 4 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
9 | 3, 4, 8 | 3syl 17 | . . 3 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
10 | df-nf 1471 | . . 3 ⊢ (Ⅎ𝑥∀𝑦𝜑 ↔ ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) | |
11 | 9, 10 | sylibr 134 | . 2 ⊢ (∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥∀𝑦𝜑) |
12 | nfal.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
13 | 11, 12 | mpg 1461 | 1 ⊢ Ⅎ𝑥∀𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1361 Ⅎwnf 1470 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-7 1458 ax-gen 1459 |
This theorem depends on definitions: df-bi 117 df-nf 1471 |
This theorem is referenced by: nfnf 1587 nfa2 1589 aaan 1597 cbv3 1752 cbv2 1759 nfald 1770 cbval2 1931 nfsb4t 2024 nfeuv 2054 mo23 2077 bm1.1 2172 nfnfc1 2332 nfnfc 2336 nfeq 2337 nfabdw 2348 sbcnestgf 3120 dfnfc2 3839 nfdisjv 4004 nfdisj1 4005 nffr 4361 exmidfodomrlemr 7214 exmidfodomrlemrALT 7215 exmidunben 12440 bdsepnft 14910 bdsepnfALT 14912 setindft 14988 strcollnft 15007 pw1nct 15024 |
Copyright terms: Public domain | W3C validator |