![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > domnsym | Structured version Unicode version |
Description: Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.) |
Ref | Expression |
---|---|
domnsym |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brdom2 7442 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sdomnsym 7539 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sdomnen 7441 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | ensym 7461 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | nsyl3 119 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 5 | jaoi 379 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 6 | sylbi 195 |
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 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-rab 2804 df-v 3073 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-op 3985 df-uni 4193 df-br 4394 df-opab 4452 df-id 4737 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-er 7204 df-en 7414 df-dom 7415 df-sdom 7416 |
This theorem is referenced by: sdom0 7546 sdomdomtr 7547 domsdomtr 7549 sdomdif 7562 onsdominel 7563 nndomo 7608 sdom1 7616 fofinf1o 7696 carddom2 8251 fidomtri 8267 fidomtri2 8268 infxpenlem 8284 alephordi 8348 infdif 8482 infdif2 8483 cfslbn 8540 cfslb2n 8541 fincssdom 8596 fin45 8665 domtriom 8716 alephval2 8840 alephreg 8850 pwcfsdom 8851 cfpwsdom 8852 pwfseqlem3 8931 gchpwdom 8941 gchaleph 8942 hargch 8944 gchhar 8950 winainflem 8964 rankcf 9048 tskcard 9052 vdwlem12 14164 odinf 16177 rectbntr0 20534 erdszelem10 27225 finminlem 28654 fphpd 29296 |
Copyright terms: Public domain | W3C validator |