Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > alnex | Structured version Visualization version Unicode 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 1705 | . 2 | |
2 | 1 | con2bii 347 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wb 196 wal 1481 wex 1704 |
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 1705 |
This theorem is referenced by: nf3 1712 nex 1731 alex 1753 2exnaln 1756 aleximi 1759 19.38 1766 alinexa 1770 alexn 1771 nexdh 1792 19.43 1810 19.43OLD 1811 19.33b 1813 nexdvOLD 1865 cbvexdva 2283 mo2v 2477 ralnex 2992 mo2icl 3385 n0el 3940 falseral0 4081 disjsn 4246 dm0rn0 5342 reldm0 5343 iotanul 5866 imadif 5973 dffv2 6271 kmlem4 8975 axpowndlem3 9421 axpownd 9423 hashgt0elex 13189 nmo 29325 bnj1143 30861 unbdqndv1 32499 bj-nexdh 32606 bj-modal5e 32636 axc11n11r 32673 bj-hbntbi 32695 bj-modal4e 32705 wl-nfeqfb 33323 wl-sb8et 33334 wl-lem-nexmo 33349 pm10.251 38559 pm10.57 38570 elnev 38639 spr0nelg 41726 zrninitoringc 42071 alimp-no-surprise 42527 |
Copyright terms: Public domain | W3C validator |