Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqsstrrid | Structured version Visualization version GIF version |
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
Ref | Expression |
---|---|
eqsstrrid.1 | ⊢ 𝐵 = 𝐴 |
eqsstrrid.2 | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Ref | Expression |
---|---|
eqsstrrid | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsstrrid.1 | . . 3 ⊢ 𝐵 = 𝐴 | |
2 | 1 | eqcomi 2830 | . 2 ⊢ 𝐴 = 𝐵 |
3 | eqsstrrid.2 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | |
4 | 2, 3 | eqsstrid 4015 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ⊆ wss 3936 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-in 3943 df-ss 3952 |
This theorem is referenced by: relcnvtrg 6119 fimacnvdisj 6557 dffv2 6756 fimacnv 6839 f1ompt 6875 abnexg 7478 fnwelem 7825 tfrlem15 8028 omxpenlem 8618 hartogslem1 9006 infxpidm2 9443 alephgeom 9508 infenaleph 9517 cfflb 9681 pwfseqlem5 10085 imasvscafn 16810 mrieqvlemd 16900 cnvps 17822 dirdm 17844 tsrdir 17848 frmdss2 18028 subdrgint 19582 iinopn 21510 neitr 21788 xkococnlem 22267 tgpconncomp 22721 trcfilu 22903 mbfconstlem 24228 itg2seq 24343 limcdif 24474 dvres2lem 24508 c1lip3 24596 lhop 24613 plyeq0 24801 dchrghm 25832 uspgrupgrushgr 26962 upgrreslem 27086 umgrreslem 27087 umgrres1 27096 umgr2v2e 27307 chssoc 29273 pmtrcnelor 30735 tocycfvres1 30752 tocycfvres2 30753 dimkerim 31023 hauseqcn 31138 carsgclctunlem3 31578 cvmliftmolem1 32528 cvmlift2lem9a 32550 cvmlift2lem9 32558 cnres2 35056 rngunsnply 39822 proot1hash 39849 clcnvlem 40032 cnvtrcl0 40035 trrelsuperrel2dg 40065 brtrclfv2 40121 imo72b2lem1 40570 fourierdlem92 42532 vsetrec 44854 |
Copyright terms: Public domain | W3C validator |