![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssint | Structured version Visualization version GIF version |
Description: Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.) |
Ref | Expression |
---|---|
ssint | ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss3 3970 | . 2 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵) | |
2 | vex 3478 | . . . 4 ⊢ 𝑦 ∈ V | |
3 | 2 | elint2 4957 | . . 3 ⊢ (𝑦 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥) |
4 | 3 | ralbii 3093 | . 2 ⊢ (∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥) |
5 | ralcom 3286 | . . 3 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥) | |
6 | dfss3 3970 | . . . 4 ⊢ (𝐴 ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥) | |
7 | 6 | ralbii 3093 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥) |
8 | 5, 7 | bitr4i 277 | . 2 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) |
9 | 1, 4, 8 | 3bitri 296 | 1 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2106 ∀wral 3061 ⊆ wss 3948 ∩ cint 4950 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-v 3476 df-in 3955 df-ss 3965 df-int 4951 |
This theorem is referenced by: ssintab 4969 ssintub 4970 iinpw 5109 oneqmini 6416 fint 6770 fnssintima 7358 sorpssint 7722 iscard2 9970 coftr 10267 isf32lem2 10348 inttsk 10768 dfrtrcl2 15008 isacs1i 17600 mrelatglb 18512 fbfinnfr 23344 fclscmp 23533 noextenddif 27168 eqscut2 27304 scutun12 27308 ssmxidllem 32584 fneint 35228 topmeet 35244 igenval2 36929 ismrcd1 41426 onintunirab 41966 dftrcl3 42461 dfrtrcl3 42474 sssalgen 45041 issalgend 45044 intubeu 47599 ipoglblem 47604 |
Copyright terms: Public domain | W3C validator |