| 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 1781. See also the dual pair df-ex 1780 / alex 1826. Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
| Ref | Expression |
|---|---|
| exnal | ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alex 1826 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
| 2 | 1 | con2bii 357 | 1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∀wal 1538 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: alexn 1845 nfnbi 1855 exanali 1859 19.35 1877 19.30 1881 nfeqf2 2382 nabbib 3045 r2exlem 3143 spc3gv 3604 vn0 4345 notzfaus 5363 dtruALT2 5370 dvdemo1 5373 dtruALT 5388 eunex 5390 reusv2lem2 5399 dtru 5441 dtruOLD 5446 brprcneu 6896 brprcneuALT 6897 dffv2 7004 zfcndpow 10656 hashfun 14476 nmo 32509 bnj1304 34833 bnj1253 35031 axrepprim 35702 axunprim 35703 axregprim 35705 axinfprim 35706 axacprim 35707 dftr6 35751 brtxpsd 35895 elfuns 35916 dfrdg4 35952 relowlpssretop 37365 onsupmaxb 43251 clsk3nimkb 44053 expandexn 44308 vk15.4j 44548 vk15.4jVD 44934 alneu 47136 |
| Copyright terms: Public domain | W3C validator |