![]() |
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 2362 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | ssab2 3087 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 3038 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ∈ wcel 1434 {cab 2069 {crab 2357 ⊆ wss 2982 |
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 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-rab 2362 df-in 2988 df-ss 2995 |
This theorem is referenced by: ssrabeq 3089 rabexg 3941 pwnss 3953 undifexmid 3984 exmidexmid 3987 onintrab2im 4290 ordtriexmidlem 4291 ontr2exmid 4296 ordtri2or2exmidlem 4297 onsucsssucexmid 4298 onsucelsucexmidlem 4300 tfis 4352 nnregexmid 4388 dmmptss 4867 ssimaex 5286 f1oresrab 5381 riotacl 5533 ssfiexmid 6432 domfiexmid 6434 genpelxp 6815 ltexprlempr 6912 cauappcvgprlemcl 6957 cauappcvgprlemladd 6962 caucvgprlemcl 6980 caucvgprprlemcl 7008 uzf 8755 supminfex 8818 rpre 8873 ixxf 9049 fzf 9161 serige0 9622 expcl2lemap 9637 expclzaplem 9649 expge0 9661 expge1 9662 dvdsflip 10459 infssuzex 10552 infssuzcldc 10554 gcddvds 10562 lcmn0cl 10657 phicl2 10797 phimullem 10808 bdrabexg 10964 |
Copyright terms: Public domain | W3C validator |