| 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 4243 exmidundif 4250 exmidundifim 4251 dmcosseq 4950 relfld 5211 imadif 5354 imain 5356 fimacnv 5709 fo2ndf 6313 tposeq 6333 tfrlemibfn 6414 tfrlemi14d 6419 tfr1onlembfn 6430 tfri1dALT 6437 tfrcllembfn 6443 dcdifsnid 6590 fisbth 6980 en2eqpr 7004 exmidpw 7005 exmidpweq 7006 undifdcss 7020 nnnninfeq2 7231 en2other2 7304 exmidontriimlem3 7335 addnqpr 7674 mulnqpr 7690 distrprg 7701 ltexpri 7726 addcanprg 7729 recexprlemex 7750 aptipr 7754 cauappcvgprlemladd 7771 fzopth 10183 fzosplit 10301 fzouzsplit 10303 zsupssdc 10381 frecuzrdgtcl 10557 frecuzrdgdomlem 10562 ccatrn 11065 phimullem 12547 structcnvcnv 12848 imasaddfnlemg 13146 gsumvallem2 13325 trivsubgd 13536 trivsubgsnd 13537 trivnsgd 13553 kerf1ghm 13610 conjnmz 13615 lspun 14164 lspsn 14178 lspsnneg 14182 lsp0 14185 lsslsp 14191 mulgrhm2 14372 znrrg 14422 eltg4i 14527 unitg 14534 tgtop 14540 tgidm 14546 basgen 14552 2basgeng 14554 epttop 14562 ntrin 14596 isopn3 14597 neiuni 14633 tgrest 14641 resttopon 14643 rest0 14651 txdis 14749 hmeontr 14785 xmettx 14982 findset 15885 pwtrufal 15938 pwf1oexmid 15940 |
| Copyright terms: Public domain | W3C validator |