Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqssd | Unicode version |
Description: Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.) |
Ref | Expression |
---|---|
eqssd.1 | |
eqssd.2 |
Ref | Expression |
---|---|
eqssd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqssd.1 | . 2 | |
2 | eqssd.2 | . 2 | |
3 | eqss 3112 | . 2 | |
4 | 1, 2, 3 | sylanbrc 413 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 wss 3071 |
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 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-in 3077 df-ss 3084 |
This theorem is referenced by: eqrd 3115 eqelssd 3116 unissel 3765 intmin 3791 int0el 3801 pwntru 4122 exmidundif 4129 exmidundifim 4130 dmcosseq 4810 relfld 5067 imadif 5203 imain 5205 fimacnv 5549 fo2ndf 6124 tposeq 6144 tfrlemibfn 6225 tfrlemi14d 6230 tfr1onlembfn 6241 tfri1dALT 6248 tfrcllembfn 6254 dcdifsnid 6400 fisbth 6777 en2eqpr 6801 exmidpw 6802 undifdcss 6811 en2other2 7052 addnqpr 7369 mulnqpr 7385 distrprg 7396 ltexpri 7421 addcanprg 7424 recexprlemex 7445 aptipr 7449 cauappcvgprlemladd 7466 fzopth 9841 fzosplit 9954 fzouzsplit 9956 frecuzrdgtcl 10185 frecuzrdgdomlem 10190 phimullem 11901 structcnvcnv 11975 eltg4i 12224 unitg 12231 tgtop 12237 tgidm 12243 basgen 12249 2basgeng 12251 epttop 12259 ntrin 12293 isopn3 12294 neiuni 12330 tgrest 12338 resttopon 12340 rest0 12348 txdis 12446 hmeontr 12482 xmettx 12679 findset 13143 pwtrufal 13192 pwf1oexmid 13194 |
Copyright terms: Public domain | W3C validator |