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 224 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
2 | pm4.72 946 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) | |
3 | elun 4127 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
4 | 3 | bibi1i 341 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
5 | 1, 2, 4 | 3bitr4i 305 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
6 | 5 | albii 1820 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
7 | dfss2 3957 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
8 | dfcleq 2817 | . 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
9 | 6, 7, 8 | 3bitr4i 305 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∨ wo 843 ∀wal 1535 = wceq 1537 ∈ wcel 2114 ∪ cun 3936 ⊆ wss 3938 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-v 3498 df-un 3943 df-in 3945 df-ss 3954 |
This theorem is referenced by: ssequn2 4161 undif 4432 uniop 5407 pwssun 5458 unisuc 6269 ordssun 6292 ordequn 6293 onun2i 6308 funiunfv 7009 sorpssun 7458 ordunpr 7543 onuninsuci 7557 domss2 8678 sucdom2 8716 findcard2s 8761 rankopb 9283 ranksuc 9296 kmlem11 9588 fin1a2lem10 9833 trclublem 14357 trclubi 14358 trclub 14360 reltrclfv 14379 modfsummods 15150 cvgcmpce 15175 mreexexlem3d 16919 dprd2da 19166 dpjcntz 19176 dpjdisj 19177 dpjlsm 19178 dpjidcl 19182 ablfac1eu 19197 perfcls 21975 dfconn2 22029 comppfsc 22142 llycmpkgen2 22160 trfil2 22497 fixufil 22532 tsmsres 22754 ustssco 22825 ustuqtop1 22852 xrge0gsumle 23443 volsup 24159 mbfss 24249 itg2cnlem2 24365 iblss2 24408 vieta1lem2 24902 amgm 25570 wilthlem2 25648 ftalem3 25654 rpvmasum2 26090 iuninc 30314 pmtrcnel 30735 pmtrcnelor 30737 hgt750lemb 31929 rankaltopb 33442 hfun 33641 bj-prmoore 34409 nacsfix 39316 fvnonrel 39964 rclexi 39982 rtrclex 39984 trclubgNEW 39985 trclubNEW 39986 dfrtrcl5 39996 trrelsuperrel2dg 40023 iunrelexp0 40054 corcltrcl 40091 isotone1 40405 aacllem 44909 |
Copyright terms: Public domain | W3C validator |