Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3sstr4g | Structured version Visualization version GIF version |
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Ref | Expression |
---|---|
3sstr4g.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
3sstr4g.2 | ⊢ 𝐶 = 𝐴 |
3sstr4g.3 | ⊢ 𝐷 = 𝐵 |
Ref | Expression |
---|---|
3sstr4g | ⊢ (𝜑 → 𝐶 ⊆ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3sstr4g.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | 3sstr4g.2 | . . 3 ⊢ 𝐶 = 𝐴 | |
3 | 3sstr4g.3 | . . 3 ⊢ 𝐷 = 𝐵 | |
4 | 2, 3 | sseq12i 3994 | . 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵) |
5 | 1, 4 | sylibr 235 | 1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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: rabss2 4051 unss2 4154 sslin 4208 intss 4888 ssopab2 5424 xpss12 5563 coss1 5719 coss2 5720 cnvss 5736 rnss 5802 ssres 5873 ssres2 5874 imass1 5957 imass2 5958 predpredss 6147 ssoprab2 7211 ressuppss 7838 tposss 7882 onovuni 7968 ss2ixp 8462 fodomfi 8785 coss12d 14320 isumsplit 15183 isumrpcl 15186 cvgrat 15227 gsumzf1o 18961 gsumzmhm 18986 gsumzinv 18994 dsmmsubg 20815 qustgpopn 22655 metnrmlem2 23395 ovolsslem 24012 uniioombllem3 24113 ulmres 24903 xrlimcnp 25473 pntlemq 26104 cusgredg 27133 sspba 28431 shlej2i 29083 chpssati 30067 iunrnmptss 30245 mptssALT 30348 pmtrcnelor 30662 bnj1408 32205 subfacp1lem6 32329 mthmpps 32726 qsss1 35426 cossss 35550 aomclem4 39535 cotrclrcl 39965 symgsubmefmndALT 43996 fldc 44282 fldcALTV 44300 |
Copyright terms: Public domain | W3C validator |