![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssequn1 | Structured version Visualization version Unicode version |
Description: A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
ssequn1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicom 205 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm4.72 892 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | elun 3586 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | bibi1i 320 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 4 | 3bitr4i 285 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | albii 1702 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | dfss2 3433 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | dfcleq 2456 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 6, 7, 8 | 3bitr4i 285 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-un 3421 df-in 3423 df-ss 3430 |
This theorem is referenced by: ssequn2 3619 undif 3860 uniop 4721 pwssun 4762 unisuc 5522 ordssun 5545 ordequn 5546 onun2i 5561 funiunfv 6183 sorpssun 6610 ordunpr 6685 onuninsuci 6699 domss2 7762 sucdom2 7799 findcard2s 7843 rankopb 8354 ranksuc 8367 kmlem11 8621 fin1a2lem10 8870 trclublem 13114 trclubi 13115 trclub 13117 reltrclfv 13136 modfsummods 13908 cvgcmpce 13933 mreexexlem3d 15607 dprd2da 17730 dpjcntz 17740 dpjdisj 17741 dpjlsm 17742 dpjidcl 17746 ablfac1eu 17761 perfcls 20436 dfcon2 20489 comppfsc 20602 llycmpkgen2 20620 trfil2 20957 fixufil 20992 tsmsres 21213 ustssco 21284 ustuqtop1 21311 xrge0gsumle 21906 volsup 22565 mbfss 22658 itg2cnlem2 22776 iblss2 22819 vieta1lem2 23320 amgm 23972 wilthlem2 24050 ftalem3 24055 rpvmasum2 24406 iuninc 28230 rankaltopb 30796 hfun 30995 nacsfix 35600 fvnonrel 36249 rclexi 36268 rtrclex 36270 trclubgNEW 36271 trclubNEW 36272 dfrtrcl5 36282 trrelsuperrel2dg 36309 iunrelexp0 36340 corcltrcl 36377 aacllem 40909 |
Copyright terms: Public domain | W3C validator |