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 3951 | . 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵) |
5 | 1, 4 | sylibr 233 | 1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ⊆ wss 3887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-in 3894 df-ss 3904 |
This theorem is referenced by: rabss2 4011 unss2 4115 sslin 4168 intss 4900 ssopab2 5459 xpss12 5604 coss1 5764 coss2 5765 cnvss 5781 rnss 5848 ssres 5918 ssres2 5919 imass1 6009 imass2 6010 predpredss 6209 predrelss 6240 ssoprab2 7343 ressuppss 7999 tposss 8043 onovuni 8173 ss2ixp 8698 fodomfi 9092 coss12d 14683 isumsplit 15552 isumrpcl 15555 cvgrat 15595 gsumzf1o 19513 gsumzmhm 19538 gsumzinv 19546 dsmmsubg 20950 qustgpopn 23271 metnrmlem2 24023 ovolsslem 24648 uniioombllem3 24749 ulmres 25547 xrlimcnp 26118 pntlemq 26749 cusgredg 27791 sspba 29089 shlej2i 29741 chpssati 30725 iunrnmptss 30905 mptssALT 31012 pmtrcnelor 31360 rspectopn 31817 zarmxt1 31830 bnj1408 33016 subfacp1lem6 33147 mthmpps 33544 bj-gabss 35123 qsss1 36423 cossss 36548 aomclem4 40882 cotrclrcl 41350 fldc 45641 fldcALTV 45659 |
Copyright terms: Public domain | W3C validator |