Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exnal | Structured version Visualization version GIF version |
Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1784. See also the dual pair df-ex 1783 / alex 1828. Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Ref | Expression |
---|---|
exnal | ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alex 1828 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 1 | con2bii 358 | 1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wal 1537 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: alexn 1847 nfnbi 1857 exanali 1862 19.35 1880 19.30 1884 nfeqf2 2377 nabbi 3047 r2exlem 3231 spc3gv 3543 vn0 4272 notzfaus 5285 dtruALT2 5293 dvdemo1 5296 dtruALT 5311 eunex 5313 reusv2lem2 5322 dtru 5359 brprcneu 6764 brprcneuALT 6765 dffv2 6863 zfcndpow 10372 hashfun 14152 nmo 30838 bnj1304 32799 bnj1253 32997 axrepprim 33643 axunprim 33644 axregprim 33646 axinfprim 33647 axacprim 33648 dftr6 33718 brtxpsd 34196 elfuns 34217 dfrdg4 34253 bj-dtru 34999 relowlpssretop 35535 sn-dtru 40188 clsk3nimkb 41650 expandexn 41907 vk15.4j 42148 vk15.4jVD 42534 alneu 44616 |
Copyright terms: Public domain | W3C validator |