|   | 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 3972 | . 2 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵) | |
| 2 | vex 3484 | . . . 4 ⊢ 𝑦 ∈ V | |
| 3 | 2 | elint2 4953 | . . 3 ⊢ (𝑦 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥) | 
| 4 | 3 | ralbii 3093 | . 2 ⊢ (∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥) | 
| 5 | ralcom 3289 | . . 3 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥) | |
| 6 | dfss3 3972 | . . . 4 ⊢ (𝐴 ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥) | |
| 7 | 6 | ralbii 3093 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥) | 
| 8 | 5, 7 | bitr4i 278 | . 2 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) | 
| 9 | 1, 4, 8 | 3bitri 297 | 1 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∈ wcel 2108 ∀wral 3061 ⊆ wss 3951 ∩ cint 4946 | 
| 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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-11 2157 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-v 3482 df-ss 3968 df-int 4947 | 
| This theorem is referenced by: ssintab 4965 ssintub 4966 iinpw 5106 oneqmini 6436 fint 6787 fnssintima 7382 sorpssint 7753 iscard2 10016 coftr 10313 isf32lem2 10394 inttsk 10814 dfrtrcl2 15101 isacs1i 17700 mrelatglb 18605 fbfinnfr 23849 fclscmp 24038 noextenddif 27713 eqscut2 27851 scutun12 27855 ssdifidllem 33484 ssmxidllem 33501 fneint 36349 topmeet 36365 igenval2 38073 ismrcd1 42709 onintunirab 43239 dftrcl3 43733 dfrtrcl3 43746 sssalgen 46350 issalgend 46353 intubeu 48873 ipoglblem 48878 | 
| Copyright terms: Public domain | W3C validator |