![]() |
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 946 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) | |
3 | elun 4147 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
4 | 3 | bibi1i 337 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
5 | 1, 2, 4 | 3bitr4i 302 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
6 | 5 | albii 1819 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
7 | dfss2 3967 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
8 | dfcleq 2723 | . 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) | |
9 | 6, 7, 8 | 3bitr4i 302 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 843 ∀wal 1537 = wceq 1539 ∈ wcel 2104 ∪ cun 3945 ⊆ wss 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-un 3952 df-in 3954 df-ss 3964 |
This theorem is referenced by: ssequn2 4182 undif 4480 uniop 5514 pwssun 5570 cnvimassrndm 6150 unisucg 6441 ordssun 6465 ordequn 6466 onunel 6468 onun2 6471 funiunfv 7249 sorpssun 7722 ordunpr 7816 onuninsuci 7831 omun 7880 sucdom2OLD 9084 domss2 9138 findcard2s 9167 sucdom2 9208 rankopb 9849 ranksuc 9862 kmlem11 10157 fin1a2lem10 10406 trclublem 14946 trclubi 14947 trclub 14949 reltrclfv 14968 modfsummods 15743 cvgcmpce 15768 mreexexlem3d 17594 dprd2da 19953 dpjcntz 19963 dpjdisj 19964 dpjlsm 19965 dpjidcl 19969 ablfac1eu 19984 perfcls 23089 dfconn2 23143 comppfsc 23256 llycmpkgen2 23274 trfil2 23611 fixufil 23646 tsmsres 23868 ustssco 23939 ustuqtop1 23966 xrge0gsumle 24569 volsup 25305 mbfss 25395 itg2cnlem2 25512 iblss2 25555 vieta1lem2 26060 amgm 26731 wilthlem2 26809 ftalem3 26815 rpvmasum2 27251 noetalem1 27480 madeoldsuc 27616 iuninc 32059 pmtrcnel 32520 pmtrcnelor 32522 hgt750lemb 33966 rankaltopb 35255 hfun 35454 bj-prmoore 36299 nacsfix 41752 cantnfresb 42376 omabs2 42384 onsucunipr 42424 oaun2 42433 oaun3 42434 fvnonrel 42650 rclexi 42668 rtrclex 42670 trclubgNEW 42671 trclubNEW 42672 dfrtrcl5 42682 trrelsuperrel2dg 42724 iunrelexp0 42755 corcltrcl 42792 isotone1 43101 aacllem 47935 |
Copyright terms: Public domain | W3C validator |