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 3143 | . 2 | |
2 | sstr2 3135 | . . . 4 | |
3 | 2 | adantl 275 | . . 3 |
4 | sstr2 3135 | . . . 4 | |
5 | 4 | adantr 274 | . . 3 |
6 | 3, 5 | impbid 128 | . 2 |
7 | 1, 6 | sylbi 120 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wceq 1335 wss 3102 |
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 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-11 1486 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-in 3108 df-ss 3115 |
This theorem is referenced by: sseq12 3153 sseq1i 3154 sseq1d 3157 nssne2 3187 sbss 3502 pwjust 3544 elpw 3549 elpwg 3551 sssnr 3716 ssprr 3719 sstpr 3720 unimax 3806 trss 4071 elssabg 4109 bnd2 4134 exmidexmid 4157 exmidsssn 4163 exmidsssnc 4164 mss 4186 exss 4187 frforeq2 4305 ordtri2orexmid 4482 ontr2exmid 4484 onsucsssucexmid 4486 reg2exmidlema 4493 sucprcreg 4508 ordtri2or2exmid 4530 ontri2orexmidim 4531 onintexmid 4532 tfis 4542 tfisi 4546 elomssom 4564 nnregexmid 4580 releq 4668 xpsspw 4698 iss 4912 relcnvtr 5105 iotass 5152 fununi 5238 funcnvuni 5239 funimaexglem 5253 ffoss 5446 ssimaex 5529 tfrlem1 6255 el2oss1o 6390 nnsucsssuc 6439 qsss 6539 phpm 6810 ssfiexmid 6821 findcard2d 6836 findcard2sd 6837 diffifi 6839 isinfinf 6842 fiintim 6873 fisseneq 6876 fidcenumlemrk 6898 fidcenumlemr 6899 sbthlem2 6902 isbth 6911 ctssdclemr 7056 onntri45 7176 elinp 7394 sup3exmid 8828 zfz1isolem1 10711 zfz1iso 10712 fimaxre2 11126 sumeq1 11252 fsum2d 11332 fsumabs 11362 fsumiun 11374 prodeq1f 11449 fprod2d 11520 exmidunben 12166 ctiunct 12180 ssomct 12185 restsspw 12372 uniopn 12410 fiinopn 12413 fiinbas 12458 baspartn 12459 eltg2 12464 eltg3 12468 topbas 12478 clsval 12522 neival 12554 neiint 12556 neipsm 12565 opnneissb 12566 opnssneib 12567 innei 12574 restbasg 12579 cnpdis 12653 txbas 12669 eltx 12670 neitx 12679 txlm 12690 blssexps 12840 blssex 12841 neibl 12902 metrest 12917 xmettx 12921 tgioo 12957 tgqioo 12958 limcimolemlt 13044 recnprss 13067 bj-om 13523 bj-2inf 13524 bj-nntrans 13537 bj-omtrans 13542 exmid1stab 13583 subctctexmid 13584 pw1nct 13586 |
Copyright terms: Public domain | W3C validator |