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 1454 | 1 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1314 ∃wex 1453 |
This theorem was proved from axioms: ax-ie1 1454 |
This theorem is referenced by: nfe1 1457 19.8a 1554 exim 1563 19.43 1592 hbex 1600 excomim 1626 19.38 1639 exan 1656 equs5e 1751 exdistrfor 1756 hbmo1 2015 euan 2033 euor2 2035 eupicka 2057 mopick2 2060 moexexdc 2061 2moex 2063 2euex 2064 2exeu 2069 2eu4 2070 2eu7 2071 |
Copyright terms: Public domain | W3C validator |