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 3928 | . 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵) |
5 | 1, 4 | mpbir 234 | 1 ⊢ 𝐶 ⊆ 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ⊆ wss 3863 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3407 df-in 3870 df-ss 3880 |
This theorem is referenced by: relopabiv 5687 rncoss 5838 imassrn 5937 rnin 6007 inimass 6015 f1ossf1o 6940 ssoprab2i 7318 omopthlem2 8382 rankval4 9480 cardf2 9556 r0weon 9623 dcomex 10058 axdc2lem 10059 fpwwe2lem1 10242 canthwe 10262 recmulnq 10575 npex 10597 axresscn 10759 trclublem 14555 bpoly4 15618 2strop1 16780 odlem1 18924 gexlem1 18965 psrbagsn 21018 bwth 22304 2ndcctbss 22349 uniioombllem4 24480 uniioombllem5 24481 eff1olem 25434 birthdaylem1 25831 nvss 28671 lediri 29615 lejdiri 29617 sshhococi 29624 mayetes3i 29807 disjxpin 30643 imadifxp 30656 sxbrsigalem5 31964 eulerpartlemmf 32051 kur14lem6 32883 cvmlift2lem12 32986 bj-xpcossxp 35092 bj-rrhatsscchat 35139 mblfinlem4 35552 lclkrs2 39289 areaquad 40748 corclrcl 40990 corcltrcl 41022 relopabVD 42192 |
Copyright terms: Public domain | W3C validator |