| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eqsstrrdi | Structured version Visualization version GIF version | ||
| Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| Ref | Expression |
|---|---|
| eqsstrrdi.1 | ⊢ (𝜑 → 𝐵 = 𝐴) |
| eqsstrrdi.2 | ⊢ 𝐵 ⊆ 𝐶 |
| Ref | Expression |
|---|---|
| eqsstrrdi | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqsstrrdi.1 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐴) | |
| 2 | 1 | eqcomd 2743 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) |
| 3 | eqsstrrdi.2 | . 2 ⊢ 𝐵 ⊆ 𝐶 | |
| 4 | 2, 3 | eqsstrdi 4028 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 |
| This theorem is referenced by: eqimsscd 4041 mptss 6060 ffvresb 7145 tposss 8252 sbthlem5 9127 rankxpl 9915 winafp 10737 wunex2 10778 iooval2 13420 telfsumo 15838 structcnvcnv 17190 ressbasssg 17282 ressbasssOLD 17285 tsrdir 18649 idresefmnd 18912 idrespermg 19429 symgsssg 19485 gsumzoppg 19962 lidlssbas 21223 dsmmsubg 21763 cnclsi 23280 txss12 23613 txbasval 23614 kqsat 23739 kqcldsat 23741 fmss 23954 cfilucfil 24572 tngtopn 24671 dvaddf 25979 dvmulf 25980 dvcof 25986 dvmptres3 25994 dvmptres2 26000 dvmptcmul 26002 dvmptcj 26006 dvcnvlem 26014 dvcnv 26015 dvcnvrelem1 26056 dvcnvrelem2 26057 plyrem 26347 ulmss 26440 ulmdvlem1 26443 ulmdvlem3 26445 ulmdv 26446 isppw 27157 dchrelbas2 27281 pw2bday 28418 chsupsn 31432 pjss1coi 32182 off2 32651 resspos 32956 resstos 32957 submomnd 33087 elrgspnsubrunlem2 33252 suborng 33345 elrspunidl 33456 evl1deg2 33602 submatres 33805 madjusmdetlem2 33827 madjusmdetlem3 33828 omsmon 34300 signstfvn 34584 elmsta 35553 mthmpps 35587 dissneqlem 37341 exrecfnlem 37380 prjcrv0 42643 hbtlem6 43141 ofoaf 43368 dvmulcncf 45940 dvdivcncf 45942 itgsubsticclem 45990 |
| Copyright terms: Public domain | W3C validator |