![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssrab3 | Structured version Visualization version GIF version |
Description: Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
ssrab3.1 | ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} |
Ref | Expression |
---|---|
ssrab3 | ⊢ 𝐵 ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrab3.1 | . 2 ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} | |
2 | ssrab2 3908 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 3854 | 1 ⊢ 𝐵 ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 {crab 3094 ⊆ wss 3792 |
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-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-rab 3099 df-in 3799 df-ss 3806 |
This theorem is referenced by: dmmptss 5885 omsson 7347 oawordeulem 7918 ordtypelem2 8713 wemapso2lem 8746 wemapwe 8891 cplem1 9049 cofsmo 9426 fin23lem28 9497 fin23lem30 9499 isf32lem5 9514 isf32lem6 9515 isf32lem7 9516 isf32lem8 9517 hsmexlem4 9586 hsmexlem5 9587 hsmexlem6 9588 zorn2lem1 9653 zorn2lem3 9655 zorn2lem4 9656 zorn2lem5 9657 0nnq 10081 elpqn 10082 rpnnen1lem2 12124 rpssre 12144 sqrlem5 14394 dvdsflip 15446 divalglem2 15525 divalglem5 15527 divalglem8 15530 gcdcllem3 15629 bezoutlem2 15663 bezoutlem3 15664 maxprmfct 15825 phimullem 15888 eulerthlem2 15891 pclem 15947 infpn2 16021 prmreclem2 16025 prmreclem3 16026 prmreclem5 16028 4sqlem13 16065 4sqlem14 16066 4sqlem17 16069 4sqlem18 16070 vdwnnlem3 16105 ramcl2lem 16117 ramtcl 16118 ramtcl2 16119 ramtub 16120 imasdsval2 16562 gsumval1 17663 nmzsubg 18019 nmznsg 18022 usgrres 26655 frgrwopregbsn 27725 frgrwopreg1 27726 eulerpartlemgvv 31036 reprpmtf1o 31306 hgt750lemb 31336 hgt750leme 31338 bnj1212 31469 bnj213 31551 bnj1286 31686 bnj1312 31725 bnj1523 31738 limcperiod 40768 cncfshift 41015 cncfperiod 41020 |
Copyright terms: Public domain | W3C validator |