![]() |
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 3078 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | sylanbrc 411 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-11 1467 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-in 3043 df-ss 3050 |
This theorem is referenced by: eqrd 3081 eqelssd 3082 unissel 3731 intmin 3757 int0el 3767 pwntru 4082 exmidundif 4089 exmidundifim 4090 dmcosseq 4768 relfld 5025 imadif 5161 imain 5163 fimacnv 5503 fo2ndf 6078 tposeq 6098 tfrlemibfn 6179 tfrlemi14d 6184 tfr1onlembfn 6195 tfri1dALT 6202 tfrcllembfn 6208 dcdifsnid 6354 fisbth 6730 en2eqpr 6754 exmidpw 6755 undifdcss 6764 en2other2 7000 addnqpr 7317 mulnqpr 7333 distrprg 7344 ltexpri 7369 addcanprg 7372 recexprlemex 7393 aptipr 7397 cauappcvgprlemladd 7414 fzopth 9734 fzosplit 9847 fzouzsplit 9849 frecuzrdgtcl 10078 frecuzrdgdomlem 10083 phimullem 11746 structcnvcnv 11818 eltg4i 12067 unitg 12074 tgtop 12080 tgidm 12086 basgen 12092 2basgeng 12094 epttop 12102 ntrin 12136 isopn3 12137 neiuni 12173 tgrest 12181 resttopon 12183 rest0 12191 txdis 12288 xmettx 12499 findset 12833 pwtrufal 12882 pwf1oexmid 12884 |
Copyright terms: Public domain | W3C validator |