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 3594 | . 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵) |
5 | 1, 4 | mpbir 220 | 1 ⊢ 𝐶 ⊆ 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 |
This theorem is referenced by: brab2a 5091 rncoss 5307 imassrn 5396 rnin 5461 inimass 5468 ssoprab2i 6647 omopthlem2 7623 rankval4 8613 cardf2 8652 r0weon 8718 dcomex 9152 axdc2lem 9153 fpwwe2lem1 9332 canthwe 9352 recmulnq 9665 npex 9687 axresscn 9848 trclublem 13582 bpoly4 14629 2strop1 15814 odlem1 17777 gexlem1 17817 psrbagsn 19316 bwth 21023 2ndcctbss 21068 uniioombllem4 23160 uniioombllem5 23161 eff1olem 24098 birthdaylem1 24478 nvss 26832 lediri 27780 lejdiri 27782 sshhococi 27789 mayetes3i 27972 disjxpin 28783 imadifxp 28796 sxbrsigalem5 29677 eulerpartlemmf 29764 kur14lem6 30447 cvmlift2lem12 30550 bj-rrhatsscchat 32300 mblfinlem4 32619 lclkrs2 35847 areaquad 36821 corclrcl 37018 corcltrcl 37050 relopabVD 38159 |
Copyright terms: Public domain | W3C validator |