![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssintub | Structured version Visualization version GIF version |
Description: Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.) |
Ref | Expression |
---|---|
ssintub | ⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssint 4728 | . 2 ⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ ∀𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}𝐴 ⊆ 𝑦) | |
2 | sseq2 3846 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑦)) | |
3 | 2 | elrab 3572 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ (𝑦 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑦)) |
4 | 3 | simprbi 492 | . 2 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} → 𝐴 ⊆ 𝑦) |
5 | 1, 4 | mprgbir 3109 | 1 ⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 {crab 3094 ⊆ wss 3792 ∩ cint 4712 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rab 3099 df-v 3400 df-in 3799 df-ss 3806 df-int 4713 |
This theorem is referenced by: intmin 4732 wuncid 9902 mrcssid 16674 lspssid 19391 lbsextlem3 19568 aspssid 19741 sscls 21279 filufint 22143 spanss2 28793 shsval2i 28835 ococin 28856 chsupsn 28861 sssigagen 30814 dynkin 30836 igenss 34494 pclssidN 36058 dochocss 37529 rgspnssid 38713 |
Copyright terms: Public domain | W3C validator |