Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sseqtrri | Unicode version |
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.) |
Ref | Expression |
---|---|
sseqtrri.1 | |
sseqtrri.2 |
Ref | Expression |
---|---|
sseqtrri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqtrri.1 | . 2 | |
2 | sseqtrri.2 | . . 3 | |
3 | 2 | eqcomi 2143 | . 2 |
4 | 1, 3 | sseqtri 3131 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1331 wss 3071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-in 3077 df-ss 3084 |
This theorem is referenced by: eqimss2i 3154 difdif2ss 3333 snsspr1 3668 snsspr2 3669 snsstp1 3670 snsstp2 3671 snsstp3 3672 prsstp12 3673 prsstp13 3674 prsstp23 3675 iunxdif2 3861 pwpwssunieq 3901 sssucid 4337 opabssxp 4613 dmresi 4874 cnvimass 4902 ssrnres 4981 cnvcnv 4991 cnvssrndm 5060 dmmpossx 6097 tfrcllemssrecs 6249 sucinc 6341 mapex 6548 exmidpw 6802 casefun 6970 djufun 6989 ressxr 7809 ltrelxr 7825 nnssnn0 8980 un0addcl 9010 un0mulcl 9011 nn0ssxnn0 9043 fzssnn 9848 fzossnn0 9952 isumclim3 11192 isprm3 11799 phimullem 11901 tgvalex 12219 cnrest2 12405 qtopbasss 12690 tgqioo 12716 |
Copyright terms: Public domain | W3C validator |