| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3sstr4i | Structured version Visualization version GIF version | ||
| Description: Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
| Ref | Expression |
|---|---|
| 3sstr4.1 | ⊢ 𝐴 ⊆ 𝐵 |
| 3sstr4.2 | ⊢ 𝐶 = 𝐴 |
| 3sstr4.3 | ⊢ 𝐷 = 𝐵 |
| Ref | Expression |
|---|---|
| 3sstr4i | ⊢ 𝐶 ⊆ 𝐷 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3sstr4.2 | . . 3 ⊢ 𝐶 = 𝐴 | |
| 2 | 3sstr4.1 | . . 3 ⊢ 𝐴 ⊆ 𝐵 | |
| 3 | 1, 2 | eqsstri 4030 | . 2 ⊢ 𝐶 ⊆ 𝐵 |
| 4 | 3sstr4.3 | . 2 ⊢ 𝐷 = 𝐵 | |
| 5 | 3, 4 | sseqtrri 4033 | 1 ⊢ 𝐶 ⊆ 𝐷 |
| Colors of variables: wff setvar class |
| Syntax hints: = 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: relopabiv 5830 rncoss 5986 imassrn 6089 rnin 6166 inimass 6175 f1ossf1o 7148 ssoprab2i 7544 omopthlem2 8698 1sdom2dom 9283 rankval4 9907 cardf2 9983 r0weon 10052 dcomex 10487 axdc2lem 10488 fpwwe2lem1 10671 canthwe 10691 recmulnq 11004 npex 11026 axresscn 11188 mpoaddf 11249 mpomulf 11250 trclublem 15034 bpoly4 16095 2strop1 17273 odlem1 19553 gexlem1 19597 pzriprnglem4 21495 psrbagsn 22087 bwth 23418 2ndcctbss 23463 uniioombllem4 25621 uniioombllem5 25622 eff1olem 26590 birthdaylem1 26994 zssno 28367 nvss 30612 lediri 31556 lejdiri 31558 sshhococi 31565 mayetes3i 31748 disjxpin 32601 imadifxp 32614 constrextdg2 33790 sxbrsigalem5 34290 eulerpartlemmf 34377 kur14lem6 35216 cvmlift2lem12 35319 bj-xpcossxp 37190 bj-rrhatsscchat 37237 mblfinlem4 37667 lclkrs2 41542 areaquad 43228 corclrcl 43720 corcltrcl 43752 relopabVD 44921 ovolval5lem3 46669 uspgrlimlem4 47958 |
| Copyright terms: Public domain | W3C validator |