Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > hbe1 | GIF version |
Description: 𝑥 is not free in ∃𝑥𝜑. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
hbe1 | ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ie1 1480 | 1 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1340 ∃wex 1479 |
This theorem was proved from axioms: ax-ie1 1480 |
This theorem is referenced by: nfe1 1483 19.8a 1577 exim 1586 19.43 1615 hbex 1623 excomim 1650 19.38 1663 exan 1680 equs5e 1782 exdistrfor 1787 hbmo1 2051 euan 2069 euor2 2071 eupicka 2093 mopick2 2096 moexexdc 2097 2moex 2099 2euex 2100 2exeu 2105 2eu4 2106 2eu7 2107 |
Copyright terms: Public domain | W3C validator |