Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqsstri | Unicode version |
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.) |
Ref | Expression |
---|---|
eqsstr.1 | |
eqsstr.2 |
Ref | Expression |
---|---|
eqsstri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsstr.2 | . 2 | |
2 | eqsstr.1 | . . 3 | |
3 | 2 | sseq1i 3163 | . 2 |
4 | 1, 3 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1342 wss 3111 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: eqsstrri 3170 ssrab2 3222 ssrab3 3223 rabssab 3225 difdifdirss 3488 ifssun 3529 opabss 4040 brab2ga 4673 relopabi 4724 dmopabss 4810 resss 4902 relres 4906 exse2 4972 rnin 5007 rnxpss 5029 cnvcnvss 5052 dmmptss 5094 cocnvss 5123 fnres 5298 resasplitss 5361 fabexg 5369 f0 5372 ffvresb 5642 isoini2 5781 dmoprabss 5915 elmpocl 6030 tposssxp 6208 dftpos4 6222 smores 6251 smores2 6253 iordsmo 6256 swoer 6520 swoord1 6521 swoord2 6522 ecss 6533 ecopovsym 6588 ecopovtrn 6589 ecopover 6590 ecopovsymg 6591 ecopovtrng 6592 ecopoverg 6593 sbthlem7 6919 caserel 7043 ctssdccl 7067 pw1on 7173 pinn 7241 niex 7244 ltrelpi 7256 dmaddpi 7257 dmmulpi 7258 enqex 7292 ltrelnq 7297 enq0ex 7371 ltrelpr 7437 enrex 7669 ltrelsr 7670 ltrelre 7765 axaddf 7800 axmulf 7801 ltrelxr 7950 lerelxr 7952 nn0ssre 9109 nn0ssz 9200 rpre 9587 fz1ssfz0 10042 cau3 11043 fsum3cvg3 11323 isumshft 11417 explecnv 11432 clim2prod 11466 ntrivcvgap 11475 dvdszrcl 11718 dvdsflip 11774 infssuzcldc 11869 phimullem 12136 eulerthlemfi 12139 eulerthlemrprm 12140 eulerthlema 12141 eulerthlemh 12142 eulerthlemth 12143 ctiunctlemuom 12312 structcnvcnv 12353 fvsetsid 12371 strleun 12426 dmtopon 12568 lmfval 12739 lmbrf 12762 cnconst2 12780 txuni2 12803 xmeter 12983 ivthinclemex 13167 dvrecap 13224 |
Copyright terms: Public domain | W3C validator |