![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseq1 | GIF version |
Description: Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
Ref | Expression |
---|---|
sseq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqss 3117 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
2 | sstr2 3109 | . . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶)) | |
3 | 2 | adantl 275 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶)) |
4 | sstr2 3109 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | |
5 | 4 | adantr 274 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) |
6 | 3, 5 | impbid 128 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) |
7 | 1, 6 | sylbi 120 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1332 ⊆ wss 3076 |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-in 3082 df-ss 3089 |
This theorem is referenced by: sseq12 3127 sseq1i 3128 sseq1d 3131 nssne2 3161 sbss 3476 pwjust 3516 elpw 3521 elpwg 3523 sssnr 3688 ssprr 3691 sstpr 3692 unimax 3778 trss 4043 elssabg 4081 bnd2 4105 exmidexmid 4128 exmidsssn 4133 exmidsssnc 4134 mss 4156 exss 4157 frforeq2 4275 ordtri2orexmid 4446 ontr2exmid 4448 onsucsssucexmid 4450 reg2exmidlema 4457 sucprcreg 4472 ordtri2or2exmid 4494 onintexmid 4495 tfis 4505 tfisi 4509 elnn 4527 nnregexmid 4542 releq 4629 xpsspw 4659 iss 4873 relcnvtr 5066 iotass 5113 fununi 5199 funcnvuni 5200 funimaexglem 5214 ffoss 5407 ssimaex 5490 tfrlem1 6213 nnsucsssuc 6396 qsss 6496 phpm 6767 ssfiexmid 6778 findcard2d 6793 findcard2sd 6794 diffifi 6796 isinfinf 6799 fiintim 6825 fisseneq 6828 fidcenumlemrk 6850 fidcenumlemr 6851 sbthlem2 6854 isbth 6863 ctssdclemr 7005 elinp 7306 sup3exmid 8739 zfz1isolem1 10615 zfz1iso 10616 fimaxre2 11030 sumeq1 11156 fsum2d 11236 fsumabs 11266 fsumiun 11278 prodeq1f 11353 exmidunben 11975 ctiunct 11989 restsspw 12169 uniopn 12207 fiinopn 12210 fiinbas 12255 baspartn 12256 eltg2 12261 eltg3 12265 topbas 12275 clsval 12319 neival 12351 neiint 12353 neipsm 12362 opnneissb 12363 opnssneib 12364 innei 12371 restbasg 12376 cnpdis 12450 txbas 12466 eltx 12467 neitx 12476 txlm 12487 blssexps 12637 blssex 12638 neibl 12699 metrest 12714 xmettx 12718 tgioo 12754 tgqioo 12755 limcimolemlt 12841 recnprss 12864 bj-om 13306 bj-2inf 13307 bj-nntrans 13320 bj-omtrans 13325 el2oss1o 13359 exmid1stab 13368 subctctexmid 13369 pw1nct 13371 |
Copyright terms: Public domain | W3C validator |