![]() |
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 4012 | . 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵) |
5 | 1, 4 | mpbir 230 | 1 ⊢ 𝐶 ⊆ 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ⊆ wss 3949 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3475 df-in 3956 df-ss 3966 |
This theorem is referenced by: relopabiv 5826 rncoss 5979 imassrn 6079 rnin 6156 inimass 6164 f1ossf1o 7143 ssoprab2i 7537 omopthlem2 8687 1sdom2dom 9278 rankval4 9898 cardf2 9974 r0weon 10043 dcomex 10478 axdc2lem 10479 fpwwe2lem1 10662 canthwe 10682 recmulnq 10995 npex 11017 axresscn 11179 mpoaddf 11240 mpomulf 11241 trclublem 14982 bpoly4 16043 2strop1 17215 odlem1 19497 gexlem1 19541 pzriprnglem4 21417 psrbagsn 22014 bwth 23334 2ndcctbss 23379 uniioombllem4 25535 uniioombllem5 25536 eff1olem 26502 birthdaylem1 26903 nvss 30423 lediri 31367 lejdiri 31369 sshhococi 31376 mayetes3i 31559 disjxpin 32399 imadifxp 32412 sxbrsigalem5 33941 eulerpartlemmf 34028 kur14lem6 34854 cvmlift2lem12 34957 bj-xpcossxp 36701 bj-rrhatsscchat 36748 mblfinlem4 37166 lclkrs2 41045 areaquad 42675 corclrcl 43168 corcltrcl 43200 relopabVD 44371 ovolval5lem3 46071 |
Copyright terms: Public domain | W3C validator |