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 3949 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐷)) |
5 | 1, 4 | mpbid 235 | 1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ⊆ wss 3881 |
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 2113 ax-9 2121 ax-ext 2709 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-v 3423 df-in 3888 df-ss 3898 |
This theorem is referenced by: cnvtsr 18119 dprdss 19441 dprd2da 19454 dmdprdsplit2lem 19457 mplind 21052 txcmplem1 22562 setsmstopn 23400 tngtopn 23572 bcthlem2 24246 bcthlem4 24248 uniiccvol 24501 dyadmaxlem 24518 dvlip2 24916 dvne0 24932 shlej2 29466 gsumzresunsn 31057 pmtrcnel2 31102 cyc3co2 31150 fedgmullem1 31448 hauseqcn 31586 bnd2lem 35713 heiborlem8 35740 dochord 39148 lclkrlem2p 39300 mapdsn 39419 hbtlem5 40685 fvmptiunrelexplb0d 40998 fvmptiunrelexplb1d 41000 isclatd 45971 |
Copyright terms: Public domain | W3C validator |