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 1743 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | 1 | con2bii 346 | 1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 ∀wal 1473 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: alexn 1760 exanali 1773 19.35 1794 19.30 1798 nfeqf2 2285 nabbi 2884 r2exlem 3041 spc3gv 3271 notzfaus 4766 dtru 4783 eunex 4785 reusv2lem2 4795 reusv2lem2OLD 4796 dtruALT 4826 dvdemo1 4829 dtruALT2 4838 brprcneu 6096 dffv2 6181 zfcndpow 9317 hashfun 13084 nmo 28709 bnj1304 30144 bnj1253 30339 axrepprim 30833 axunprim 30834 axregprim 30836 axinfprim 30837 axacprim 30838 dftr6 30893 brtxpsd 31171 elfuns 31192 dfrdg4 31228 bj-dtru 31985 bj-eunex 31987 bj-dvdemo1 31990 relowlpssretop 32388 wl-dveeq12 32490 clsk3nimkb 37358 vk15.4j 37755 vk15.4jVD 38172 alneu 39850 |
Copyright terms: Public domain | W3C validator |