![]() |
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 3979 | . 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵) |
5 | 1, 4 | mpbir 230 | 1 ⊢ 𝐶 ⊆ 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ⊆ wss 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 |
This theorem is referenced by: relopabiv 5781 rncoss 5932 imassrn 6029 rnin 6104 inimass 6112 f1ossf1o 7079 ssoprab2i 7472 omopthlem2 8611 1sdom2dom 9198 rankval4 9810 cardf2 9886 r0weon 9955 dcomex 10390 axdc2lem 10391 fpwwe2lem1 10574 canthwe 10594 recmulnq 10907 npex 10929 axresscn 11091 trclublem 14887 bpoly4 15949 2strop1 17118 odlem1 19324 gexlem1 19368 psrbagsn 21487 bwth 22777 2ndcctbss 22822 uniioombllem4 24966 uniioombllem5 24967 eff1olem 25920 birthdaylem1 26317 nvss 29577 lediri 30521 lejdiri 30523 sshhococi 30530 mayetes3i 30713 disjxpin 31548 imadifxp 31561 sxbrsigalem5 32928 eulerpartlemmf 33015 kur14lem6 33845 cvmlift2lem12 33948 bj-xpcossxp 35689 bj-rrhatsscchat 35736 mblfinlem4 36147 lclkrs2 40032 areaquad 41579 corclrcl 42053 corcltrcl 42085 relopabVD 43257 ovolval5lem3 44969 |
Copyright terms: Public domain | W3C validator |