| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ax5e | Structured version Visualization version GIF version | ||
| Description: A rephrasing of ax-5 1910 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.) |
| Ref | Expression |
|---|---|
| ax5e | ⊢ (∃𝑥𝜑 → 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 1910 | . 2 ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑) | |
| 2 | eximal 1782 | . 2 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | |
| 3 | 1, 2 | mpbir 231 | 1 ⊢ (∃𝑥𝜑 → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∀wal 1538 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: ax5ea 1913 exlimiv 1930 exlimdv 1933 19.21v 1939 19.23v 1942 19.36imv 1945 19.41v 1949 19.9v 1983 aeveq 2056 sbv 2088 sbequ2 2249 mo4 2566 rspn0 4356 relopabi 5832 lfuhgr3 35125 bj-cbvalim 36646 bj-cbvexim 36647 bj-cbvexivw 36673 bj-eqs 36676 bj-nnfv 36755 bj-snsetex 36964 bj-snglss 36971 topdifinffinlem 37348 ac6s6f 38180 ismnushort 44320 fnchoice 45034 ormklocald 46889 natlocalincr 46891 |
| Copyright terms: Public domain | W3C validator |