New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > alex | Unicode version |
Description: Theorem 19.6 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
alex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot 282 | . . 3 | |
2 | 1 | albii 1566 | . 2 |
3 | alnex 1543 | . 2 | |
4 | 2, 3 | bitri 240 | 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 ax-gen 1546 ax-5 1557 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: 2nalexn 1573 exnal 1574 19.3v 1665 hba1 1786 exists2 2294 nnsucelrlem1 4424 ltfinex 4464 eqpwrelk 4478 ncfinlowerlem1 4482 eqtfinrelk 4486 evenfinex 4503 oddfinex 4504 evenodddisjlem1 4515 nnadjoinlem1 4519 srelk 4524 sfintfinlem1 4531 tfinnnlem1 4533 dfop2lem1 4573 funsex 5828 qsexg 5982 |
Copyright terms: Public domain | W3C validator |