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 1753 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 1 | con2bii 347 | 1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∀wal 1481 ∃wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: alexn 1771 exanali 1786 19.35 1805 19.30 1809 nfeqf2 2297 nabbi 2896 r2exlem 3059 spc3gv 3298 notzfaus 4840 dtru 4857 eunex 4859 reusv2lem2 4869 reusv2lem2OLD 4870 dtruALT 4899 dvdemo1 4902 dtruALT2 4911 brprcneu 6184 dffv2 6271 zfcndpow 9438 hashfun 13224 nmo 29325 bnj1304 30890 bnj1253 31085 axrepprim 31579 axunprim 31580 axregprim 31582 axinfprim 31583 axacprim 31584 dftr6 31640 brtxpsd 32001 elfuns 32022 dfrdg4 32058 bj-dtru 32797 bj-eunex 32799 bj-dvdemo1 32802 relowlpssretop 33212 wl-dveeq12 33311 clsk3nimkb 38338 vk15.4j 38734 vk15.4jVD 39150 alneu 41201 |
Copyright terms: Public domain | W3C validator |