New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > exnal | Unicode version |
Description: Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
exnal |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alex 1572 | . 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 ax-gen 1546 ax-5 1557 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: alexn 1579 exanali 1585 19.30 1604 excom 1741 ax12olem5 1931 ax10lem2 1937 equsex 1962 spc3gv 2944 necompl 3544 opkelimagekg 4271 dfpw2 4327 dfaddc2 4381 nnsucelrlem1 4424 eqpw1relk 4479 eqtfinrelk 4486 setconslem2 4732 setconslem3 4733 setconslem7 4737 dfswap2 4741 nfunv 5138 brimage 5793 releqel 5807 releqmpt2 5809 ovcelem1 6171 tcfnex 6244 nchoicelem10 6298 fnfreclem1 6317 |
Copyright terms: Public domain | W3C validator |