![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alnex | Structured version Visualization version GIF version |
Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.) |
Ref | Expression |
---|---|
alnex | ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex 1853 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
2 | 1 | con2bii 346 | 1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∀wal 1629 ∃wex 1852 |
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 197 df-ex 1853 |
This theorem is referenced by: nf3 1860 nex 1879 alex 1901 2exnaln 1904 aleximi 1907 19.38 1914 alinexa 1920 alexn 1921 nexdh 1943 19.43 1962 19.43OLD 1963 19.33b 1965 nexdvOLD 2017 cbvex 2433 cbvexv 2435 cbvexd 2437 cbvexdva 2441 mo2v 2625 ralnex 3141 mo2icl 3538 n0el 4088 falseral0 4221 disjsn 4384 dm0rn0 5481 reldm0 5482 iotanul 6010 imadif 6114 dffv2 6414 kmlem4 9178 axpowndlem3 9624 axpownd 9626 hashgt0elex 13392 iswspthsnon 26987 nmo 29666 bnj1143 31200 unbdqndv1 32837 bj-nexdh 32944 axc11n11r 33011 bj-hbntbi 33033 bj-modal4e 33043 wl-nfeqfb 33659 wl-sb8et 33670 wl-lem-nexmo 33684 pm10.251 39086 pm10.57 39097 elnev 39166 spr0nelg 42255 zrninitoringc 42600 alimp-no-surprise 43059 |
Copyright terms: Public domain | W3C validator |