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 1788. See also the dual pair df-ex 1787 / alex 1832. Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Ref | Expression |
---|---|
exnal | ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alex 1832 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 1 | con2bii 361 | 1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 ∀wal 1540 ∃wex 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 |
This theorem depends on definitions: df-bi 210 df-ex 1787 |
This theorem is referenced by: alexn 1851 nfnbi 1861 exanali 1866 19.35 1884 19.30 1888 nfeqf2 2377 nabbi 3036 r2exlem 3212 spc3gv 3508 vn0 4227 notzfaus 5228 notzfausOLD 5229 dtru 5237 dvdemo1 5240 dtruALT 5255 eunex 5257 reusv2lem2 5266 dtruALT2 5302 brprcneu 6665 fvprc 6666 dffv2 6763 zfcndpow 10116 hashfun 13890 nmo 30412 bnj1304 32370 bnj1253 32568 axrepprim 33214 axunprim 33215 axregprim 33217 axinfprim 33218 axacprim 33219 dftr6 33289 brtxpsd 33834 elfuns 33855 dfrdg4 33891 bj-dtru 34630 relowlpssretop 35158 sn-dtru 39779 clsk3nimkb 41196 expandexn 41449 vk15.4j 41686 vk15.4jVD 42072 alneu 44149 |
Copyright terms: Public domain | W3C validator |