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 2425 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | ssab2 3181 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | |
3 | 1, 2 | eqsstri 3129 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ∈ wcel 1480 {cab 2125 {crab 2420 ⊆ wss 3071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rab 2425 df-in 3077 df-ss 3084 |
This theorem is referenced by: ssrabeq 3183 rabexg 4071 pwnss 4083 undifexmid 4117 exmidexmid 4120 exmidsssnc 4126 onintrab2im 4434 ordtriexmidlem 4435 ontr2exmid 4440 ordtri2or2exmidlem 4441 onsucsssucexmid 4442 onsucelsucexmidlem 4444 tfis 4497 nnregexmid 4534 dmmptss 5035 ssimaex 5482 f1oresrab 5585 riotacl 5744 pmvalg 6553 ssfiexmid 6770 domfiexmid 6772 ctssdccl 6996 ctssexmid 7024 genpelxp 7319 ltexprlempr 7416 cauappcvgprlemcl 7461 cauappcvgprlemladd 7466 caucvgprlemcl 7484 caucvgprprlemcl 7512 suplocexprlemex 7530 uzf 9329 supminfex 9392 rpre 9448 ixxf 9681 fzf 9794 expcl2lemap 10305 expclzaplem 10317 expge0 10329 expge1 10330 dvdsflip 11549 infssuzex 11642 infssuzcldc 11644 gcddvds 11652 lcmn0cl 11749 phicl2 11890 phimullem 11901 ennnfonelemg 11916 ennnfonelemh 11917 ctiunctlemuom 11949 epttop 12259 neipsm 12323 cnpfval 12364 blfvalps 12554 blfps 12578 blf 12579 divcnap 12724 cdivcncfap 12756 cnopnap 12763 ivthinclemex 12789 limcdifap 12800 dvfgg 12826 dvidlemap 12829 dvcnp2cntop 12832 dvaddxxbr 12834 dvmulxxbr 12835 dvcoapbr 12840 dvrecap 12846 bdrabexg 13104 subctctexmid 13196 |
Copyright terms: Public domain | W3C validator |