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 211 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
2 | pm4.72 916 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) | |
3 | elun 3715 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
4 | 3 | bibi1i 327 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
5 | 1, 2, 4 | 3bitr4i 291 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
6 | 5 | albii 1737 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
7 | dfss2 3557 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
8 | dfcleq 2604 | . 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
9 | 6, 7, 8 | 3bitr4i 291 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∀wal 1473 = wceq 1475 ∈ wcel 1977 ∪ cun 3538 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-in 3547 df-ss 3554 |
This theorem is referenced by: ssequn2 3748 undif 4001 uniop 4902 pwssun 4944 unisuc 5718 ordssun 5744 ordequn 5745 onun2i 5760 funiunfv 6410 sorpssun 6842 ordunpr 6918 onuninsuci 6932 domss2 8004 sucdom2 8041 findcard2s 8086 rankopb 8598 ranksuc 8611 kmlem11 8865 fin1a2lem10 9114 trclublem 13582 trclubi 13583 trclubiOLD 13584 trclub 13587 reltrclfv 13606 modfsummods 14366 cvgcmpce 14391 mreexexlem3d 16129 dprd2da 18264 dpjcntz 18274 dpjdisj 18275 dpjlsm 18276 dpjidcl 18280 ablfac1eu 18295 perfcls 20979 dfcon2 21032 comppfsc 21145 llycmpkgen2 21163 trfil2 21501 fixufil 21536 tsmsres 21757 ustssco 21828 ustuqtop1 21855 xrge0gsumle 22444 volsup 23131 mbfss 23219 itg2cnlem2 23335 iblss2 23378 vieta1lem2 23870 amgm 24517 wilthlem2 24595 ftalem3 24601 rpvmasum2 25001 iuninc 28761 rankaltopb 31256 hfun 31455 nacsfix 36293 fvnonrel 36922 rclexi 36941 rtrclex 36943 trclubgNEW 36944 trclubNEW 36945 dfrtrcl5 36955 trrelsuperrel2dg 36982 iunrelexp0 37013 corcltrcl 37050 isotone1 37366 aacllem 42356 |
Copyright terms: Public domain | W3C validator |