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 2969 | . 2 |
4 | 1, 3 | mpbir 134 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1243 wss 2917 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-11 1397 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-in 2924 df-ss 2931 |
This theorem is referenced by: eqsstr3i 2976 ssrab2 3025 rabssab 3027 difdifdirss 3307 opabss 3821 brab2ga 4415 relopabi 4463 dmopabss 4547 resss 4635 relres 4639 exse2 4699 rnin 4733 rnxpss 4754 cnvcnvss 4775 dmmptss 4817 fnres 5015 resasplitss 5069 fabexg 5077 f0 5080 ffvresb 5328 isoini2 5458 dmoprabss 5586 elmpt2cl 5698 tposssxp 5864 dftpos4 5878 smores 5907 smores2 5909 iordsmo 5912 swoer 6134 swoord1 6135 swoord2 6136 ecss 6147 ecopovsym 6202 ecopovtrn 6203 ecopover 6204 ecopovsymg 6205 ecopovtrng 6206 ecopoverg 6207 pinn 6407 niex 6410 ltrelpi 6422 dmaddpi 6423 dmmulpi 6424 enqex 6458 ltrelnq 6463 enq0ex 6537 ltrelpr 6603 enrex 6822 ltrelsr 6823 ltrelre 6909 ltrelxr 7080 lerelxr 7082 nn0ssre 8185 nn0ssz 8263 rpre 8589 cau3 9711 |
Copyright terms: Public domain | W3C validator |