Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssid | GIF version |
Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Ref | Expression |
---|---|
ssid | ⊢ 𝐴 ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴) | |
2 | 1 | ssriv 3101 | 1 ⊢ 𝐴 ⊆ 𝐴 |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1480 ⊆ 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-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 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-in 3077 df-ss 3084 |
This theorem is referenced by: ssidd 3118 eqimssi 3153 eqimss2i 3154 inv1 3399 difid 3431 undifabs 3439 pwidg 3524 elssuni 3764 unimax 3770 intmin 3791 rintm 3905 iunpw 4401 sucprcreg 4464 tfisi 4501 peano5 4512 xpss1 4649 xpss2 4650 residm 4851 resdm 4858 resmpt3 4868 ssrnres 4981 cocnvss 5064 dffn3 5283 fimacnv 5549 foima2 5653 tfrlem1 6205 rdgss 6280 fpmg 6568 findcard2d 6785 findcard2sd 6786 f1finf1o 6835 fidcenumlemr 6843 casef 6973 nnnninf 7023 1idprl 7398 1idpru 7399 ltexprlemm 7408 suplocexprlemmu 7526 elq 9414 expcl 10311 serclim0 11074 fsum2d 11204 fsumabs 11234 fsumiun 11246 reef11 11406 ressid 12020 topopn 12175 fiinbas 12216 topbas 12236 topcld 12278 ntrtop 12297 opnneissb 12324 opnssneib 12325 opnneiid 12333 idcn 12381 cnconst2 12402 lmres 12417 retopbas 12692 cnopncntop 12706 abscncf 12741 recncf 12742 imcncf 12743 cjcncf 12744 mulc1cncf 12745 cncfcn1cntop 12750 cncfmpt2fcntop 12754 addccncf 12755 cdivcncfap 12756 negfcncf 12758 expcncf 12761 cnrehmeocntop 12762 cnlimcim 12809 cnlimc 12810 cnlimci 12811 dvcnp2cntop 12832 dvcn 12833 dvef 12856 efcn 12857 |
Copyright terms: Public domain | W3C validator |