| 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.2 | . . 3 ⊢ 𝐶 = 𝐴 | |
| 2 | 3sstr4g.1 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
| 3 | 1, 2 | eqsstrid 4022 | . 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐵) |
| 4 | 3sstr4g.3 | . 2 ⊢ 𝐷 = 𝐵 | |
| 5 | 3, 4 | sseqtrrdi 4025 | 1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 |
| This theorem is referenced by: rabss2 4078 unss2 4187 sslin 4243 intss 4969 ssopab2 5551 xpss12 5700 coss1 5866 coss2 5867 cnvss 5883 rnss 5950 ssres 6021 ssres2 6022 imass1 6119 imass2 6120 predpredss 6328 predrelss 6358 ssoprab2 7501 ressuppss 8208 tposss 8252 onovuni 8382 ss2ixp 8950 fodomfi 9350 fodomfiOLD 9370 coss12d 15011 isumsplit 15876 isumrpcl 15879 cvgrat 15919 gsumzf1o 19930 gsumzmhm 19955 gsumzinv 19963 fldc 20785 dsmmsubg 21763 qustgpopn 24128 metnrmlem2 24882 ovolsslem 25519 uniioombllem3 25620 ulmres 26431 xrlimcnp 27011 pntlemq 27645 cusgredg 29441 sspba 30746 shlej2i 31398 chpssati 32382 iunrnmptss 32578 mptssALT 32685 pmtrcnelor 33111 rspectopn 33866 zarmxt1 33879 bnj1408 35050 subfacp1lem6 35190 mthmpps 35587 bj-gabss 36936 qsss1 38290 cossss 38426 disjdmqscossss 38804 aomclem4 43069 cotrclrcl 43755 ovnsslelem 46575 isubgredgss 47851 uspgrimprop 47873 fldcALTV 48248 |
| Copyright terms: Public domain | W3C validator |