![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseq2d | Unicode version |
Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
sseq1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sseq2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sseq2 3194 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-in 3150 df-ss 3157 |
This theorem is referenced by: sseq12d 3201 sseqtrd 3208 exmidsssn 4220 exmidsssnc 4221 onsucsssucexmid 4544 sbcrel 4730 funimass2 5313 fnco 5343 fnssresb 5347 fnimaeq0 5356 foimacnv 5498 fvelimab 5593 ssimaexg 5599 fvmptss2 5612 rdgss 6408 tapeq2 7282 summodclem2 11422 summodc 11423 zsumdc 11424 fsum3cvg3 11436 prodmodclem2 11617 prodmodc 11618 zproddc 11619 ennnfoneleminc 12462 tgval 12767 releqgg 13159 eqgex 13160 eqgfval 13161 opprsubgg 13434 unitsubm 13469 subrngpropd 13563 subrgsubm 13581 issubrg3 13594 subrgpropd 13595 lsslss 13697 lsspropdg 13747 islidlm 13795 rspcl 13807 rspssid 13808 isbasisg 14001 tgss3 14035 restbasg 14125 tgrest 14126 restopn2 14140 cnpnei 14176 cnptopresti 14195 txbas 14215 elmopn 14403 neibl 14448 dvfgg 14614 |
Copyright terms: Public domain | W3C validator |