Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssrab2 | GIF version |
Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) |
Ref | Expression |
---|---|
ssrab2 | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 2357 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | ssab2 3078 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 3029 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ∈ wcel 1433 {cab 2067 {crab 2352 ⊆ wss 2973 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-sb 1686 df-clab 2068 df-cleq 2074 df-clel 2077 df-nfc 2208 df-rab 2357 df-in 2979 df-ss 2986 |
This theorem is referenced by: ssrabeq 3080 rabexg 3921 pwnss 3933 onintrab2im 4262 ordtriexmidlem 4263 ontr2exmid 4268 ordtri2or2exmidlem 4269 onsucsssucexmid 4270 onsucelsucexmidlem 4272 tfis 4324 nnregexmid 4360 dmmptss 4837 ssimaex 5255 f1oresrab 5350 riotacl 5502 ssfiexmid 6361 domfiexmid 6363 genpelxp 6701 ltexprlempr 6798 cauappcvgprlemcl 6843 cauappcvgprlemladd 6848 caucvgprlemcl 6866 caucvgprprlemcl 6894 uzf 8622 supminfex 8685 rpre 8740 ixxf 8921 fzf 9033 serige0 9473 expcl2lemap 9488 expclzaplem 9500 expge0 9512 expge1 9513 dvdsflip 10251 infssuzex 10345 infssuzcldc 10347 gcddvds 10355 lcmn0cl 10450 bdrabexg 10697 |
Copyright terms: Public domain | W3C validator |