![]() |
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.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | 3sstr4.2 | . . 3 ⊢ 𝐶 = 𝐴 | |
3 | 3sstr4.3 | . . 3 ⊢ 𝐷 = 𝐵 | |
4 | 2, 3 | sseq12i 4009 | . 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵) |
5 | 1, 4 | mpbir 230 | 1 ⊢ 𝐶 ⊆ 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ⊆ wss 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-ss 3963 |
This theorem is referenced by: relopabiv 5818 rncoss 5971 imassrn 6072 rnin 6150 inimass 6158 f1ossf1o 7134 ssoprab2i 7528 omopthlem2 8682 1sdom2dom 9274 rankval4 9903 cardf2 9979 r0weon 10048 dcomex 10481 axdc2lem 10482 fpwwe2lem1 10665 canthwe 10685 recmulnq 10998 npex 11020 axresscn 11182 mpoaddf 11243 mpomulf 11244 trclublem 14995 bpoly4 16056 2strop1 17236 odlem1 19529 gexlem1 19573 pzriprnglem4 21470 psrbagsn 22072 bwth 23402 2ndcctbss 23447 uniioombllem4 25603 uniioombllem5 25604 eff1olem 26572 birthdaylem1 26976 zssno 28328 nvss 30523 lediri 31467 lejdiri 31469 sshhococi 31476 mayetes3i 31659 disjxpin 32508 imadifxp 32521 sxbrsigalem5 34135 eulerpartlemmf 34222 kur14lem6 35052 cvmlift2lem12 35155 bj-xpcossxp 36909 bj-rrhatsscchat 36956 mblfinlem4 37374 lclkrs2 41252 areaquad 42918 corclrcl 43411 corcltrcl 43443 relopabVD 44614 ovolval5lem3 46311 |
Copyright terms: Public domain | W3C validator |