![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqsstri | GIF 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 3196 | . 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
4 | 1, 3 | mpbir 146 | 1 ⊢ 𝐴 ⊆ 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1364 ⊆ wss 3144 |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-in 3150 df-ss 3157 |
This theorem is referenced by: eqsstrri 3203 ssrab2 3255 ssrab3 3256 rabssab 3258 difdifdirss 3522 ifssun 3563 opabss 4082 brab2ga 4719 relopabi 4770 dmopabss 4857 resss 4949 relres 4953 exse2 5020 rnin 5056 rnxpss 5078 cnvcnvss 5101 dmmptss 5143 cocnvss 5172 fnres 5351 resasplitss 5414 fabexg 5422 f0 5425 ffvresb 5699 isoini2 5840 dmoprabss 5977 elmpocl 6090 tposssxp 6273 dftpos4 6287 smores 6316 smores2 6318 iordsmo 6321 swoer 6586 swoord1 6587 swoord2 6588 ecss 6601 ecopovsym 6656 ecopovtrn 6657 ecopover 6658 ecopovsymg 6659 ecopovtrng 6660 ecopoverg 6661 sbthlem7 6991 caserel 7115 ctssdccl 7139 pw1on 7254 pinn 7337 niex 7340 ltrelpi 7352 dmaddpi 7353 dmmulpi 7354 enqex 7388 ltrelnq 7393 enq0ex 7467 ltrelpr 7533 enrex 7765 ltrelsr 7766 ltrelre 7861 axaddf 7896 axmulf 7897 ltrelxr 8047 lerelxr 8049 nn0ssre 9209 nn0ssz 9300 rpre 9689 fz1ssfz0 10146 cau3 11155 fsum3cvg3 11435 isumshft 11529 explecnv 11544 clim2prod 11578 ntrivcvgap 11587 dvdszrcl 11830 dvdsflip 11888 infssuzcldc 11983 phimullem 12256 eulerthlemfi 12259 eulerthlemrprm 12260 eulerthlema 12261 eulerthlemh 12262 eulerthlemth 12263 4sqlem1 12419 4sqlem19 12440 ctiunctlemuom 12486 structcnvcnv 12527 fvsetsid 12545 strleun 12613 dmtopon 13975 lmfval 14144 lmbrf 14167 cnconst2 14185 txuni2 14208 xmeter 14388 ivthinclemex 14572 dvrecap 14629 2sqlem7 14921 |
Copyright terms: Public domain | W3C validator |