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 3994 | . 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵) |
5 | 1, 4 | mpbir 232 | 1 ⊢ 𝐶 ⊆ 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-in 3940 df-ss 3949 |
This theorem is referenced by: relopabiv 5686 rncoss 5836 imassrn 5933 rnin 5998 inimass 6005 f1ossf1o 6882 ssoprab2i 7252 omopthlem2 8272 rankval4 9284 cardf2 9360 r0weon 9426 dcomex 9857 axdc2lem 9858 fpwwe2lem1 10041 canthwe 10061 recmulnq 10374 npex 10396 axresscn 10558 trclublem 14343 bpoly4 15401 2strop1 16595 odlem1 18592 gexlem1 18633 psrbagsn 20203 bwth 21946 2ndcctbss 21991 uniioombllem4 24114 uniioombllem5 24115 eff1olem 25059 birthdaylem1 25456 nvss 28297 lediri 29241 lejdiri 29243 sshhococi 29250 mayetes3i 29433 disjxpin 30266 imadifxp 30279 sxbrsigalem5 31445 eulerpartlemmf 31532 kur14lem6 32355 cvmlift2lem12 32458 bj-rrhatsscchat 34410 mblfinlem4 34813 lclkrs2 38556 areaquad 39701 corclrcl 39930 corcltrcl 39962 relopabVD 41112 |
Copyright terms: Public domain | W3C validator |