Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssequn1 | Structured version Visualization version GIF 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 221 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
2 | pm4.72 947 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) | |
3 | elun 4083 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
4 | 3 | bibi1i 339 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
5 | 1, 2, 4 | 3bitr4i 303 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
6 | 5 | albii 1822 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
7 | dfss2 3907 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
8 | dfcleq 2731 | . 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
9 | 6, 7, 8 | 3bitr4i 303 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 844 ∀wal 1537 = wceq 1539 ∈ wcel 2106 ∪ cun 3885 ⊆ wss 3887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-un 3892 df-in 3894 df-ss 3904 |
This theorem is referenced by: ssequn2 4117 undif 4415 uniop 5429 pwssun 5485 cnvimassrndm 6055 unisuc 6342 ordssun 6365 ordequn 6366 onun2 6370 funiunfv 7121 sorpssun 7583 ordunpr 7673 onuninsuci 7687 sucdom2OLD 8869 domss2 8923 findcard2s 8948 sucdom2 8989 rankopb 9610 ranksuc 9623 kmlem11 9916 fin1a2lem10 10165 trclublem 14706 trclubi 14707 trclub 14709 reltrclfv 14728 modfsummods 15505 cvgcmpce 15530 mreexexlem3d 17355 dprd2da 19645 dpjcntz 19655 dpjdisj 19656 dpjlsm 19657 dpjidcl 19661 ablfac1eu 19676 perfcls 22516 dfconn2 22570 comppfsc 22683 llycmpkgen2 22701 trfil2 23038 fixufil 23073 tsmsres 23295 ustssco 23366 ustuqtop1 23393 xrge0gsumle 23996 volsup 24720 mbfss 24810 itg2cnlem2 24927 iblss2 24970 vieta1lem2 25471 amgm 26140 wilthlem2 26218 ftalem3 26224 rpvmasum2 26660 iuninc 30900 pmtrcnel 31358 pmtrcnelor 31360 hgt750lemb 32636 onunel 33689 noetalem1 33944 madeoldsuc 34067 rankaltopb 34281 hfun 34480 bj-prmoore 35286 nacsfix 40534 nlimsuc 41048 fvnonrel 41205 rclexi 41223 rtrclex 41225 trclubgNEW 41226 trclubNEW 41227 dfrtrcl5 41237 trrelsuperrel2dg 41279 iunrelexp0 41310 corcltrcl 41347 isotone1 41658 aacllem 46505 |
Copyright terms: Public domain | W3C validator |