![]() |
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 1663 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con2bii 334 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 189 df-ex 1663 |
This theorem is referenced by: nex 1677 alex 1697 2exnaln 1700 aleximi 1703 19.38 1711 alinexa 1712 alexn 1713 nexdh 1724 19.43 1744 19.43OLD 1745 19.33b 1747 nexdv 1781 nf4 2042 mo2v 2305 mo2icl 3216 disjsn 4031 dm0rn0 5050 reldm0 5051 iotanul 5560 imadif 5656 dffv2 5936 kmlem4 8580 axpowndlem3 9021 axpownd 9023 hashgt0elex 12575 nmo 28114 bnj1143 29595 bj-nf3 31186 bj-nexdh 31207 bj-modal5e 31242 bj-hbntbi 31291 bj-modal4e 31301 wl-nfeqfb 31863 wl-sb8et 31874 wl-lem-nexmo 31889 n0el 32427 pm10.251 36703 pm10.57 36714 elnev 36783 falseral0 38980 zrninitoringc 40060 alimp-no-surprise 40507 |
Copyright terms: Public domain | W3C validator |