![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alnex | Structured version Visualization version GIF version |
Description: Universal quantification of negation is equivalent to negation of existential quantification. Dual of exnal 1821 (but does not depend on ax-4 1803 contrary to it). See also the dual pair df-ex 1774 / alex 1820. Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.) |
Ref | Expression |
---|---|
alnex | ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex 1774 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
2 | 1 | con2bii 356 | 1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wal 1531 ∃wex 1773 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-ex 1774 |
This theorem is referenced by: nf3 1780 nfntht2 1788 nex 1794 alex 1820 2exnaln 1823 aleximi 1826 19.38 1833 alinexa 1837 alexn 1839 nexdh 1860 19.43 1877 19.43OLD 1878 19.33b 1880 empty 1901 cbvexdvaw 2034 19.8aw 2045 nsb 2096 cbvexdw 2330 cbvexv1 2333 cbvex 2393 cbvexd 2402 dfmoeu 2525 nexmo 2530 euae 2650 ralnex 3068 issetft 3485 mo2icl 3709 n0el 4363 falseral0 4521 disjsn 4718 axprlem5 5429 dm0rn0 5929 reldm0 5932 iotanul 6529 imadif 6640 dffv2 6996 kmlem4 10182 axpowndlem3 10628 axpownd 10630 hashgt0elex 14398 zrninitoringc 20614 nmo 32306 bnj1143 34426 unbdqndv1 35988 bj-nexdh 36109 axc11n11r 36165 bj-hbntbi 36186 bj-modal4e 36197 wl-nfeqfb 37008 wl-sb8eft 37023 wl-sb8et 37025 wl-lem-nexmo 37039 wl-issetft 37054 hashnexinj 41603 onsupmaxb 42670 pm10.251 43800 pm10.57 43811 elnev 43878 spr0nelg 46818 alimp-no-surprise 48265 |
Copyright terms: Public domain | W3C validator |