Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3sstr3d | Structured version Visualization version GIF version |
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.) |
Ref | Expression |
---|---|
3sstr3d.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
3sstr3d.2 | ⊢ (𝜑 → 𝐴 = 𝐶) |
3sstr3d.3 | ⊢ (𝜑 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
3sstr3d | ⊢ (𝜑 → 𝐶 ⊆ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3sstr3d.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | 3sstr3d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐶) | |
3 | 3sstr3d.3 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐷) | |
4 | 2, 3 | sseq12d 3597 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐷)) |
5 | 1, 4 | mpbid 221 | 1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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: cnvtsr 17045 dprdss 18251 dprd2da 18264 dmdprdsplit2lem 18267 mplind 19323 txcmplem1 21254 setsmstopn 22093 tngtopn 22264 bcthlem2 22930 bcthlem4 22932 uniiccvol 23154 dyadmaxlem 23171 dvlip2 23562 dvne0 23578 shlej2 27604 hauseqcn 29269 bnd2lem 32760 heiborlem8 32787 dochord 35677 lclkrlem2p 35829 mapdsn 35948 hbtlem5 36717 fvmptiunrelexplb0d 36995 fvmptiunrelexplb1d 36997 usgrumgruspgr 40410 |
Copyright terms: Public domain | W3C validator |