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 1484 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | 2 | hbal 1438 | . 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) |
4 | 3 | nfi 1423 | 1 ⊢ Ⅎ𝑥∀𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: ∀wal 1314 Ⅎwnf 1421 |
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 1408 ax-7 1409 ax-gen 1410 ax-4 1472 |
This theorem depends on definitions: df-bi 116 df-nf 1422 |
This theorem is referenced by: nfnf 1541 nfa2 1543 aaan 1551 cbv3 1705 cbv2 1710 nfald 1718 cbval2 1873 nfsb4t 1967 nfeuv 1995 mo23 2018 bm1.1 2102 nfnfc1 2261 nfnfc 2265 nfeq 2266 sbcnestgf 3021 dfnfc2 3724 nfdisjv 3888 nfdisj1 3889 nffr 4241 exmidfodomrlemr 7026 exmidfodomrlemrALT 7027 exmidunben 11866 bdsepnft 13012 bdsepnfALT 13014 setindft 13090 strcollnft 13109 strcollnfALT 13111 |
Copyright terms: Public domain | W3C validator |