![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exnal | Structured version Visualization version GIF version |
Description: Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Ref | Expression |
---|---|
exnal | ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alex 1902 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 1 | con2bii 346 | 1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∀wal 1630 ∃wex 1853 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 |
This theorem depends on definitions: df-bi 197 df-ex 1854 |
This theorem is referenced by: alexn 1920 exanali 1935 19.35 1954 19.30 1958 nfeqf2 2442 nabbi 3034 r2exlem 3197 spc3gv 3438 notzfaus 4989 dtru 5006 eunex 5008 reusv2lem2 5018 reusv2lem2OLD 5019 dtruALT 5048 dvdemo1 5051 dtruALT2 5060 brprcneu 6345 dffv2 6433 zfcndpow 9630 hashfun 13416 nmo 29634 bnj1304 31197 bnj1253 31392 axrepprim 31886 axunprim 31887 axregprim 31889 axinfprim 31890 axacprim 31891 dftr6 31947 brtxpsd 32307 elfuns 32328 dfrdg4 32364 bj-dtru 33103 bj-eunex 33105 bj-dvdemo1 33108 relowlpssretop 33523 wl-dveeq12 33624 clsk3nimkb 38840 vk15.4j 39236 vk15.4jVD 39649 alneu 41707 |
Copyright terms: Public domain | W3C validator |