![]() |
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 949 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) | |
3 | elun 4147 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
4 | 3 | bibi1i 339 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
5 | 1, 2, 4 | 3bitr4i 303 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
6 | 5 | albii 1822 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
7 | dfss2 3967 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
8 | dfcleq 2726 | . 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
9 | 6, 7, 8 | 3bitr4i 303 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 846 ∀wal 1540 = wceq 1542 ∈ wcel 2107 ∪ cun 3945 ⊆ wss 3947 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3952 df-in 3954 df-ss 3964 |
This theorem is referenced by: ssequn2 4182 undif 4480 uniop 5514 pwssun 5570 cnvimassrndm 6148 unisucg 6439 ordssun 6463 ordequn 6464 onunel 6466 onun2 6469 funiunfv 7242 sorpssun 7715 ordunpr 7809 onuninsuci 7824 omun 7873 sucdom2OLD 9078 domss2 9132 findcard2s 9161 sucdom2 9202 rankopb 9843 ranksuc 9856 kmlem11 10151 fin1a2lem10 10400 trclublem 14938 trclubi 14939 trclub 14941 reltrclfv 14960 modfsummods 15735 cvgcmpce 15760 mreexexlem3d 17586 dprd2da 19904 dpjcntz 19914 dpjdisj 19915 dpjlsm 19916 dpjidcl 19920 ablfac1eu 19935 perfcls 22851 dfconn2 22905 comppfsc 23018 llycmpkgen2 23036 trfil2 23373 fixufil 23408 tsmsres 23630 ustssco 23701 ustuqtop1 23728 xrge0gsumle 24331 volsup 25055 mbfss 25145 itg2cnlem2 25262 iblss2 25305 vieta1lem2 25806 amgm 26475 wilthlem2 26553 ftalem3 26559 rpvmasum2 26995 noetalem1 27224 madeoldsuc 27359 iuninc 31770 pmtrcnel 32228 pmtrcnelor 32230 hgt750lemb 33606 rankaltopb 34889 hfun 35088 bj-prmoore 35934 nacsfix 41383 cantnfresb 42007 omabs2 42015 onsucunipr 42055 oaun2 42064 oaun3 42065 fvnonrel 42281 rclexi 42299 rtrclex 42301 trclubgNEW 42302 trclubNEW 42303 dfrtrcl5 42313 trrelsuperrel2dg 42355 iunrelexp0 42386 corcltrcl 42423 isotone1 42732 aacllem 47750 |
Copyright terms: Public domain | W3C validator |