![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > exnal | Structured version Unicode version |
Description: Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Ref | Expression |
---|---|
exnal |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alex 1618 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con2bii 332 |
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 ax-gen 1592 ax-4 1603 |
This theorem depends on definitions: df-bi 185 df-ex 1588 |
This theorem is referenced by: alexn 1632 exanali 1638 19.35 1655 19.30 1660 excom 1789 nfeqf2 2001 nabbi 2784 nabbiOLD 2785 spc3gv 3166 notzfaus 4574 dtru 4590 eunex 4592 reusv2lem2 4601 dtruALT 4631 dvdemo1 4634 dtruALT2 4643 brprcneu 5791 dffv2 5872 zfcndpow 8893 hashfun 12316 nmo 26020 axrepprim 27496 axunprim 27497 axregprim 27499 axinfprim 27500 axacprim 27501 dftr6 27703 brtxpsd 28068 elfuns 28089 dfrdg4 28124 alneu 30172 vk15.4j 31550 vk15.4jVD 31967 bnj1304 32130 bnj1253 32325 bj-dtru 32635 bj-eunex 32637 bj-dvdemo1 32640 |
Copyright terms: Public domain | W3C validator |