New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > alnex | Unicode version |
Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
alnex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex 1542 | . 2 | |
2 | 1 | con2bii 322 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wb 176 wal 1540 wex 1541 |
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 177 df-ex 1542 |
This theorem is referenced by: nex 1555 alex 1572 exim 1575 alinexa 1578 alexn 1579 nexdh 1589 19.35 1600 19.43 1605 19.43OLD 1606 19.33b 1608 19.38 1794 nf4 1868 mo 2226 mo2 2233 2mo 2282 axi11e 2332 mo2icl 3015 disjsn 3786 dfimak2 4298 iotanul 4354 dm0rn0 4921 dmeq0 4922 imadif 5171 |
Copyright terms: Public domain | W3C validator |