![]() |
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 3170 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sstr2 3162 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | adantl 277 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | sstr2 3162 |
. . . 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 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: sseq12 3180 sseq1i 3181 sseq1d 3184 nssne2 3214 sbss 3531 pwjust 3575 elpw 3580 elpwg 3582 sssnr 3751 ssprr 3754 sstpr 3755 unimax 3841 trss 4107 elssabg 4145 bnd2 4170 exmidexmid 4193 exmidsssn 4199 exmidsssnc 4200 mss 4222 exss 4223 frforeq2 4341 ordtri2orexmid 4518 ontr2exmid 4520 onsucsssucexmid 4522 reg2exmidlema 4529 sucprcreg 4544 ordtri2or2exmid 4566 ontri2orexmidim 4567 onintexmid 4568 tfis 4578 tfisi 4582 elomssom 4600 nnregexmid 4616 releq 4704 xpsspw 4734 iss 4948 relcnvtr 5143 iotass 5190 fununi 5279 funcnvuni 5280 funimaexglem 5294 ffoss 5488 ssimaex 5572 tfrlem1 6302 el2oss1o 6437 nnsucsssuc 6486 qsss 6587 phpm 6858 ssfiexmid 6869 findcard2d 6884 findcard2sd 6885 diffifi 6887 isinfinf 6890 fiintim 6921 fisseneq 6924 fidcenumlemrk 6946 fidcenumlemr 6947 sbthlem2 6950 isbth 6959 ctssdclemr 7104 onntri45 7233 elinp 7451 sup3exmid 8890 zfz1isolem1 10791 zfz1iso 10792 fimaxre2 11206 sumeq1 11334 fsum2d 11414 fsumabs 11444 fsumiun 11456 prodeq1f 11531 fprod2d 11602 exmidunben 12397 ctiunct 12411 ssomct 12416 restsspw 12633 uniopn 13132 fiinopn 13135 fiinbas 13180 baspartn 13181 eltg2 13186 eltg3 13190 topbas 13200 clsval 13244 neival 13276 neiint 13278 neipsm 13287 opnneissb 13288 opnssneib 13289 innei 13296 restbasg 13301 cnpdis 13375 txbas 13391 eltx 13392 neitx 13401 txlm 13412 blssexps 13562 blssex 13563 neibl 13624 metrest 13639 xmettx 13643 tgioo 13679 tgqioo 13680 limcimolemlt 13766 recnprss 13789 bj-om 14311 bj-2inf 14312 bj-nntrans 14325 bj-omtrans 14330 exmid1stab 14372 subctctexmid 14373 pw1nct 14375 |
Copyright terms: Public domain | W3C validator |