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 3082 | . 2 | |
4 | 1, 2, 3 | sylanbrc 413 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 wss 3041 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: eqrd 3085 eqelssd 3086 unissel 3735 intmin 3761 int0el 3771 pwntru 4092 exmidundif 4099 exmidundifim 4100 dmcosseq 4780 relfld 5037 imadif 5173 imain 5175 fimacnv 5517 fo2ndf 6092 tposeq 6112 tfrlemibfn 6193 tfrlemi14d 6198 tfr1onlembfn 6209 tfri1dALT 6216 tfrcllembfn 6222 dcdifsnid 6368 fisbth 6745 en2eqpr 6769 exmidpw 6770 undifdcss 6779 en2other2 7020 addnqpr 7337 mulnqpr 7353 distrprg 7364 ltexpri 7389 addcanprg 7392 recexprlemex 7413 aptipr 7417 cauappcvgprlemladd 7434 fzopth 9796 fzosplit 9909 fzouzsplit 9911 frecuzrdgtcl 10140 frecuzrdgdomlem 10145 phimullem 11812 structcnvcnv 11886 eltg4i 12135 unitg 12142 tgtop 12148 tgidm 12154 basgen 12160 2basgeng 12162 epttop 12170 ntrin 12204 isopn3 12205 neiuni 12241 tgrest 12249 resttopon 12251 rest0 12259 txdis 12357 hmeontr 12393 xmettx 12590 findset 13039 pwtrufal 13088 pwf1oexmid 13090 |
Copyright terms: Public domain | W3C validator |