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 3107 | . 2 | |
2 | sstr2 3099 | . . . 4 | |
3 | 2 | adantl 275 | . . 3 |
4 | sstr2 3099 | . . . 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 1331 wss 3066 |
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 2119 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-in 3072 df-ss 3079 |
This theorem is referenced by: sseq12 3117 sseq1i 3118 sseq1d 3121 nssne2 3151 sbss 3466 pwjust 3506 elpw 3511 elpwg 3513 sssnr 3675 ssprr 3678 sstpr 3679 unimax 3765 trss 4030 elssabg 4068 bnd2 4092 exmidexmid 4115 exmidsssn 4120 exmidsssnc 4121 mss 4143 exss 4144 frforeq2 4262 ordtri2orexmid 4433 ontr2exmid 4435 onsucsssucexmid 4437 reg2exmidlema 4444 sucprcreg 4459 ordtri2or2exmid 4481 onintexmid 4482 tfis 4492 tfisi 4496 elnn 4514 nnregexmid 4529 releq 4616 xpsspw 4646 iss 4860 relcnvtr 5053 iotass 5100 fununi 5186 funcnvuni 5187 funimaexglem 5201 ffoss 5392 ssimaex 5475 tfrlem1 6198 nnsucsssuc 6381 qsss 6481 phpm 6752 ssfiexmid 6763 findcard2d 6778 findcard2sd 6779 diffifi 6781 isinfinf 6784 fiintim 6810 fisseneq 6813 fidcenumlemrk 6835 fidcenumlemr 6836 sbthlem2 6839 isbth 6848 ctssdclemr 6990 elinp 7275 sup3exmid 8708 zfz1isolem1 10576 zfz1iso 10577 fimaxre2 10991 sumeq1 11117 fsum2d 11197 fsumabs 11227 fsumiun 11239 prodeq1f 11314 exmidunben 11928 ctiunct 11942 restsspw 12119 uniopn 12157 fiinopn 12160 fiinbas 12205 baspartn 12206 eltg2 12211 eltg3 12215 topbas 12225 clsval 12269 neival 12301 neiint 12303 neipsm 12312 opnneissb 12313 opnssneib 12314 innei 12321 restbasg 12326 cnpdis 12400 txbas 12416 eltx 12417 neitx 12426 txlm 12437 blssexps 12587 blssex 12588 neibl 12649 metrest 12664 xmettx 12668 tgioo 12704 tgqioo 12705 limcimolemlt 12791 recnprss 12814 bj-om 13124 bj-2inf 13125 bj-nntrans 13138 bj-omtrans 13143 el2oss1o 13177 exmid1stab 13184 subctctexmid 13185 |
Copyright terms: Public domain | W3C validator |