![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseq1d | Unicode version |
Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
sseq1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sseq1d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sseq1 3178 |
. 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 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: sseq12d 3186 eqsstrd 3191 snssgOLD 3727 ssiun2s 3928 treq 4104 onsucsssucexmid 4522 funimass1 5288 feq1 5343 sbcfg 5359 fvmptssdm 5595 fvimacnvi 5625 nnsucsssuc 6486 ereq1 6535 elpm2r 6659 fipwssg 6971 nnnninf 7117 ctssexmid 7141 iscnp 13332 iscnp4 13351 cnntr 13358 cnconst2 13366 cnptopresti 13371 cnptoprest 13372 txbas 13391 txcnp 13404 txdis 13410 txdis1cn 13411 blssps 13560 blss 13561 ssblex 13564 blin2 13565 metss2 13631 metrest 13639 metcnp3 13644 cnopnap 13727 limccl 13761 ellimc3apf 13762 |
Copyright terms: Public domain | W3C validator |