![]() |
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 3170 |
. 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 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: eqrd 3173 eqelssd 3174 unissel 3836 intmin 3862 int0el 3872 pwntru 4196 exmidundif 4203 exmidundifim 4204 dmcosseq 4893 relfld 5152 imadif 5291 imain 5293 fimacnv 5640 fo2ndf 6221 tposeq 6241 tfrlemibfn 6322 tfrlemi14d 6327 tfr1onlembfn 6338 tfri1dALT 6345 tfrcllembfn 6351 dcdifsnid 6498 fisbth 6876 en2eqpr 6900 exmidpw 6901 exmidpweq 6902 undifdcss 6915 nnnninfeq2 7120 en2other2 7188 exmidontriimlem3 7215 addnqpr 7538 mulnqpr 7554 distrprg 7565 ltexpri 7590 addcanprg 7593 recexprlemex 7614 aptipr 7618 cauappcvgprlemladd 7635 fzopth 10034 fzosplit 10150 fzouzsplit 10152 frecuzrdgtcl 10385 frecuzrdgdomlem 10390 zsupssdc 11925 phimullem 12195 structcnvcnv 12448 eltg4i 13188 unitg 13195 tgtop 13201 tgidm 13207 basgen 13213 2basgeng 13215 epttop 13223 ntrin 13257 isopn3 13258 neiuni 13294 tgrest 13302 resttopon 13304 rest0 13312 txdis 13410 hmeontr 13446 xmettx 13643 findset 14319 pwtrufal 14369 pwf1oexmid 14371 |
Copyright terms: Public domain | W3C validator |