![]() |
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 4964 | . 2 ⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ ∀𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}𝐴 ⊆ 𝑦) | |
2 | sseq2 4005 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑦)) | |
3 | 2 | elrab 3680 | . . 3 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ (𝑦 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑦)) |
4 | 3 | simprbi 495 | . 2 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} → 𝐴 ⊆ 𝑦) |
5 | 1, 4 | mprgbir 3058 | 1 ⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 {crab 3419 ⊆ wss 3946 ∩ cint 4946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-11 2147 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rab 3420 df-v 3464 df-ss 3963 df-int 4947 |
This theorem is referenced by: intmin 4968 cofon2 8695 naddunif 8715 wuncid 10777 mrcssid 17625 lspssid 20958 lbsextlem3 21137 aspssid 21871 sscls 23048 filufint 23912 spanss2 31275 shsval2i 31317 ococin 31338 chsupsn 31343 fldgenssid 33168 sssigagen 33991 dynkin 34013 igenss 37776 pclssidN 39607 dochocss 41078 rgspnssid 42868 intubeu 48346 |
Copyright terms: Public domain | W3C validator |