![]() |
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 3025 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | sylanbrc 408 |
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 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-11 1438 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-in 2990 df-ss 2997 |
This theorem is referenced by: eqrd 3028 unissel 3656 intmin 3682 int0el 3692 exmidundif 3999 dmcosseq 4662 relfld 4913 imadif 5047 imain 5049 fimacnv 5373 fo2ndf 5927 tposeq 5944 tfrlemibfn 6025 tfrlemi14d 6030 tfr1onlembfn 6041 tfri1dALT 6048 tfrcllembfn 6054 dcdifsnid 6195 fisbth 6529 en2eqpr 6550 exmidpw 6551 undifdcss 6560 en2other2 6725 addnqpr 7023 mulnqpr 7039 distrprg 7050 ltexpri 7075 addcanprg 7078 recexprlemex 7099 aptipr 7103 cauappcvgprlemladd 7120 fzopth 9369 fzosplit 9477 fzouzsplit 9479 frecuzrdgtcl 9708 frecuzrdgdomlem 9713 phimullem 10981 findset 11183 |
Copyright terms: Public domain | W3C validator |