| 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 3208 |
. 2
| |
| 4 | 1, 2, 3 | sylanbrc 417 |
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 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-11 1529 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-in 3172 df-ss 3179 |
| This theorem is referenced by: eqrd 3211 eqelssd 3212 unissel 3879 intmin 3905 int0el 3915 pwntru 4244 exmidundif 4251 exmidundifim 4252 dmcosseq 4951 relfld 5212 imadif 5355 imain 5357 fimacnv 5711 fo2ndf 6315 tposeq 6335 tfrlemibfn 6416 tfrlemi14d 6421 tfr1onlembfn 6432 tfri1dALT 6439 tfrcllembfn 6445 dcdifsnid 6592 fisbth 6982 en2eqpr 7006 exmidpw 7007 exmidpweq 7008 undifdcss 7022 nnnninfeq2 7233 en2other2 7306 exmidontriimlem3 7337 addnqpr 7676 mulnqpr 7692 distrprg 7703 ltexpri 7728 addcanprg 7731 recexprlemex 7752 aptipr 7756 cauappcvgprlemladd 7773 fzopth 10185 fzosplit 10303 fzouzsplit 10305 zsupssdc 10383 frecuzrdgtcl 10559 frecuzrdgdomlem 10564 ccatrn 11068 phimullem 12580 structcnvcnv 12881 imasaddfnlemg 13179 gsumvallem2 13358 trivsubgd 13569 trivsubgsnd 13570 trivnsgd 13586 kerf1ghm 13643 conjnmz 13648 lspun 14197 lspsn 14211 lspsnneg 14215 lsp0 14218 lsslsp 14224 mulgrhm2 14405 znrrg 14455 eltg4i 14560 unitg 14567 tgtop 14573 tgidm 14579 basgen 14585 2basgeng 14587 epttop 14595 ntrin 14629 isopn3 14630 neiuni 14666 tgrest 14674 resttopon 14676 rest0 14684 txdis 14782 hmeontr 14818 xmettx 15015 findset 15918 pwtrufal 15971 pwf1oexmid 15973 |
| Copyright terms: Public domain | W3C validator |