![]() |
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 1745 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
2 | 1 | con2bii 346 | 1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∀wal 1521 ∃wex 1744 |
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 1745 |
This theorem is referenced by: nf3 1752 nex 1771 alex 1793 2exnaln 1796 aleximi 1799 19.38 1806 alinexa 1810 alexn 1811 nexdh 1832 19.43 1850 19.43OLD 1851 19.33b 1853 nexdvOLD 1905 cbvexdva 2319 mo2v 2505 ralnex 3021 mo2icl 3418 n0el 3973 falseral0 4114 disjsn 4278 dm0rn0 5374 reldm0 5375 iotanul 5904 imadif 6011 dffv2 6310 kmlem4 9013 axpowndlem3 9459 axpownd 9461 hashgt0elex 13227 iswspthsnon 26806 nmo 29453 bnj1143 30987 unbdqndv1 32624 bj-nexdh 32731 bj-modal5e 32761 axc11n11r 32798 bj-hbntbi 32820 bj-modal4e 32830 wl-nfeqfb 33453 wl-sb8et 33464 wl-lem-nexmo 33479 pm10.251 38876 pm10.57 38887 elnev 38956 spr0nelg 42051 zrninitoringc 42396 alimp-no-surprise 42855 |
Copyright terms: Public domain | W3C validator |