| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > sseq1 | Unicode version | ||
| Description: Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
| Ref | Expression |
|---|---|
| sseq1 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqss 3207 |
. 2
| |
| 2 | sstr2 3199 |
. . . 4
| |
| 3 | 2 | adantl 277 |
. . 3
|
| 4 | sstr2 3199 |
. . . 4
| |
| 5 | 4 | adantr 276 |
. . 3
|
| 6 | 3, 5 | impbid 129 |
. 2
|
| 7 | 1, 6 | sylbi 121 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-11 1528 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-in 3171 df-ss 3178 |
| This theorem is referenced by: sseq12 3217 sseq1i 3218 sseq1d 3221 nssne2 3251 sbss 3567 pwjust 3616 elpw 3621 elpwg 3623 sssnr 3793 ssprr 3796 sstpr 3797 unimax 3883 trss 4150 elssabg 4191 bnd2 4216 exmidexmid 4239 exmidsssn 4245 exmidsssnc 4246 exmid1stab 4251 mss 4269 exss 4270 frforeq2 4391 ordtri2orexmid 4570 ontr2exmid 4572 onsucsssucexmid 4574 reg2exmidlema 4581 sucprcreg 4596 ordtri2or2exmid 4618 ontri2orexmidim 4619 onintexmid 4620 tfis 4630 tfisi 4634 elomssom 4652 nnregexmid 4668 releq 4756 xpsspw 4786 iss 5004 relcnvtr 5201 iotass 5248 fununi 5341 funcnvuni 5342 funimaexglem 5356 ffoss 5553 ssimaex 5639 tfrlem1 6393 el2oss1o 6528 nnsucsssuc 6577 qsss 6680 phpm 6961 ssfiexmid 6972 findcard2d 6987 findcard2sd 6988 diffifi 6990 isinfinf 6993 fiintim 7027 fisseneq 7030 fidcenumlemrk 7055 fidcenumlemr 7056 sbthlem2 7059 isbth 7068 ctssdclemr 7213 onntri45 7352 tapeq1 7363 elinp 7586 sup3exmid 9029 zfz1isolem1 10983 zfz1iso 10984 fimaxre2 11509 sumeq1 11637 fsum2d 11717 fsumabs 11747 fsumiun 11759 prodeq1f 11834 fprod2d 11905 exmidunben 12768 ctiunct 12782 ssomct 12787 restsspw 13052 lspval 14123 uniopn 14444 fiinopn 14447 fiinbas 14492 baspartn 14493 eltg2 14496 eltg3 14500 topbas 14510 clsval 14554 neival 14586 neiint 14588 neipsm 14597 opnneissb 14598 opnssneib 14599 innei 14606 restbasg 14611 cnpdis 14685 txbas 14701 eltx 14702 neitx 14711 txlm 14722 blssexps 14872 blssex 14873 neibl 14934 metrest 14949 xmettx 14953 tgioo 14997 tgqioo 14998 limcimolemlt 15107 recnprss 15130 dvmptfsum 15168 bj-om 15835 bj-2inf 15836 bj-nntrans 15849 bj-omtrans 15854 subctctexmid 15899 domomsubct 15900 pw1nct 15902 |
| Copyright terms: Public domain | W3C validator |