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 225 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
2 | pm4.72 949 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) | |
3 | elun 4049 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
4 | 3 | bibi1i 342 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
5 | 1, 2, 4 | 3bitr4i 306 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
6 | 5 | albii 1826 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
7 | dfss2 3873 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
8 | dfcleq 2732 | . 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
9 | 6, 7, 8 | 3bitr4i 306 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∨ wo 846 ∀wal 1540 = wceq 1542 ∈ wcel 2114 ∪ cun 3851 ⊆ wss 3853 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3402 df-un 3858 df-in 3860 df-ss 3870 |
This theorem is referenced by: ssequn2 4083 undif 4381 uniop 5382 pwssun 5435 cnvimassrndm 5994 unisuc 6258 ordssun 6281 ordequn 6282 onun2 6286 funiunfv 7030 sorpssun 7486 ordunpr 7572 onuninsuci 7586 sucdom2 8688 domss2 8738 findcard2s 8776 rankopb 9366 ranksuc 9379 kmlem11 9672 fin1a2lem10 9921 trclublem 14456 trclubi 14457 trclub 14459 reltrclfv 14478 modfsummods 15253 cvgcmpce 15278 mreexexlem3d 17032 dprd2da 19295 dpjcntz 19305 dpjdisj 19306 dpjlsm 19307 dpjidcl 19311 ablfac1eu 19326 perfcls 22128 dfconn2 22182 comppfsc 22295 llycmpkgen2 22313 trfil2 22650 fixufil 22685 tsmsres 22907 ustssco 22978 ustuqtop1 23005 xrge0gsumle 23597 volsup 24320 mbfss 24410 itg2cnlem2 24527 iblss2 24570 vieta1lem2 25071 amgm 25740 wilthlem2 25818 ftalem3 25824 rpvmasum2 26260 iuninc 30486 pmtrcnel 30947 pmtrcnelor 30949 hgt750lemb 32218 onunel 33275 noetalem1 33599 madeoldsuc 33722 rankaltopb 33936 hfun 34135 bj-prmoore 34939 nacsfix 40146 fvnonrel 40790 rclexi 40808 rtrclex 40810 trclubgNEW 40811 trclubNEW 40812 dfrtrcl5 40822 trrelsuperrel2dg 40865 iunrelexp0 40896 corcltrcl 40933 isotone1 41244 aacllem 46005 |
Copyright terms: Public domain | W3C validator |