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 3093 | . 2 |
4 | 1, 3 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1316 wss 3041 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: eqsstrri 3100 ssrab2 3152 rabssab 3154 difdifdirss 3417 opabss 3962 brab2ga 4584 relopabi 4635 dmopabss 4721 resss 4813 relres 4817 exse2 4883 rnin 4918 rnxpss 4940 cnvcnvss 4963 dmmptss 5005 cocnvss 5034 fnres 5209 resasplitss 5272 fabexg 5280 f0 5283 ffvresb 5551 isoini2 5688 dmoprabss 5821 elmpocl 5936 tposssxp 6114 dftpos4 6128 smores 6157 smores2 6159 iordsmo 6162 swoer 6425 swoord1 6426 swoord2 6427 ecss 6438 ecopovsym 6493 ecopovtrn 6494 ecopover 6495 ecopovsymg 6496 ecopovtrng 6497 ecopoverg 6498 sbthlem7 6819 caserel 6940 ctssdccl 6964 pinn 7085 niex 7088 ltrelpi 7100 dmaddpi 7101 dmmulpi 7102 enqex 7136 ltrelnq 7141 enq0ex 7215 ltrelpr 7281 enrex 7513 ltrelsr 7514 ltrelre 7609 axaddf 7644 axmulf 7645 ltrelxr 7793 lerelxr 7795 nn0ssre 8949 nn0ssz 9040 rpre 9416 fz1ssfz0 9865 cau3 10855 fsum3cvg3 11133 isumshft 11227 explecnv 11242 dvdszrcl 11425 dvdsflip 11476 infssuzcldc 11571 phimullem 11828 ctiunctlemuom 11876 structcnvcnv 11902 fvsetsid 11920 strleun 11975 dmtopon 12117 lmfval 12288 lmbrf 12311 cnconst2 12329 txuni2 12352 xmeter 12532 ivthinclemex 12716 dvrecap 12773 |
Copyright terms: Public domain | W3C validator |