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 1497. (Revised by Gino Giotto, 25-Aug-2024.) |
Ref | Expression |
---|---|
nfal.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfal | ⊢ Ⅎ𝑥∀𝑦𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nf 1448 | . . . . . 6 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) | |
2 | 1 | biimpi 119 | . . . . 5 ⊢ (Ⅎ𝑥𝜑 → ∀𝑥(𝜑 → ∀𝑥𝜑)) |
3 | 2 | alimi 1442 | . . . 4 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑)) |
4 | ax-7 1435 | . . . 4 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)) | |
5 | ax-5 1434 | . . . . . 6 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)) | |
6 | ax-7 1435 | . . . . . 6 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑) | |
7 | 5, 6 | syl6 33 | . . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
8 | 7 | alimi 1442 | . . . 4 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
9 | 3, 4, 8 | 3syl 17 | . . 3 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) |
10 | df-nf 1448 | . . 3 ⊢ (Ⅎ𝑥∀𝑦𝜑 ↔ ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) | |
11 | 9, 10 | sylibr 133 | . 2 ⊢ (∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥∀𝑦𝜑) |
12 | nfal.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
13 | 11, 12 | mpg 1438 | 1 ⊢ Ⅎ𝑥∀𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1340 Ⅎwnf 1447 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-7 1435 ax-gen 1436 |
This theorem depends on definitions: df-bi 116 df-nf 1448 |
This theorem is referenced by: nfnf 1564 nfa2 1566 aaan 1574 cbv3 1729 cbv2 1736 nfald 1747 cbval2 1908 nfsb4t 2001 nfeuv 2031 mo23 2054 bm1.1 2149 nfnfc1 2309 nfnfc 2313 nfeq 2314 nfabdw 2325 sbcnestgf 3091 dfnfc2 3801 nfdisjv 3965 nfdisj1 3966 nffr 4321 exmidfodomrlemr 7149 exmidfodomrlemrALT 7150 exmidunben 12302 bdsepnft 13610 bdsepnfALT 13612 setindft 13688 strcollnft 13707 pw1nct 13724 |
Copyright terms: Public domain | W3C validator |