| 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 3208 |
. 2
| |
| 2 | sstr2 3200 |
. . . 4
| |
| 3 | 2 | adantl 277 |
. . 3
|
| 4 | sstr2 3200 |
. . . 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 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-11 1529 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-in 3172 df-ss 3179 |
| This theorem is referenced by: sseq12 3218 sseq1i 3219 sseq1d 3222 nssne2 3252 sbss 3568 pwjust 3617 elpw 3622 elpwg 3624 sssnr 3794 ssprr 3797 sstpr 3798 unimax 3884 trss 4151 elssabg 4192 bnd2 4217 exmidexmid 4240 exmidsssn 4246 exmidsssnc 4247 exmid1stab 4252 mss 4270 exss 4271 frforeq2 4392 ordtri2orexmid 4571 ontr2exmid 4573 onsucsssucexmid 4575 reg2exmidlema 4582 sucprcreg 4597 ordtri2or2exmid 4619 ontri2orexmidim 4620 onintexmid 4621 tfis 4631 tfisi 4635 elomssom 4653 nnregexmid 4669 releq 4757 xpsspw 4787 iss 5005 relcnvtr 5202 iotass 5249 fununi 5342 funcnvuni 5343 funimaexglem 5357 ffoss 5554 ssimaex 5640 tfrlem1 6394 el2oss1o 6529 nnsucsssuc 6578 qsss 6681 phpm 6962 ssfiexmid 6973 findcard2d 6988 findcard2sd 6989 diffifi 6991 isinfinf 6994 fiintim 7028 fisseneq 7031 fidcenumlemrk 7056 fidcenumlemr 7057 sbthlem2 7060 isbth 7069 ctssdclemr 7214 onntri45 7353 tapeq1 7364 elinp 7587 sup3exmid 9030 zfz1isolem1 10985 zfz1iso 10986 fimaxre2 11538 sumeq1 11666 fsum2d 11746 fsumabs 11776 fsumiun 11788 prodeq1f 11863 fprod2d 11934 exmidunben 12797 ctiunct 12811 ssomct 12816 restsspw 13081 lspval 14152 uniopn 14473 fiinopn 14476 fiinbas 14521 baspartn 14522 eltg2 14525 eltg3 14529 topbas 14539 clsval 14583 neival 14615 neiint 14617 neipsm 14626 opnneissb 14627 opnssneib 14628 innei 14635 restbasg 14640 cnpdis 14714 txbas 14730 eltx 14731 neitx 14740 txlm 14751 blssexps 14901 blssex 14902 neibl 14963 metrest 14978 xmettx 14982 tgioo 15026 tgqioo 15027 limcimolemlt 15136 recnprss 15159 dvmptfsum 15197 bj-om 15873 bj-2inf 15874 bj-nntrans 15887 bj-omtrans 15892 subctctexmid 15937 domomsubct 15938 pw1nct 15940 |
| Copyright terms: Public domain | W3C validator |