![]() |
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 2742 | . 2 ⊢ 𝐴 = 𝐵 |
3 | eqsstrrid.2 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | |
4 | 2, 3 | eqsstrid 4028 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ⊆ wss 3946 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3953 df-ss 3963 |
This theorem is referenced by: relcnvtrg 6257 fimacnvdisj 6759 dffv2 6975 fimacnvOLD 7060 f1ompt 7098 abnexg 7730 fnwelem 8104 tfrlem15 8379 omxpenlem 9061 hartogslem1 9524 ttrcltr 9698 dfttrcl2 9706 infxpidm2 9999 alephgeom 10064 infenaleph 10073 cfflb 10241 pwfseqlem5 10645 imasvscafn 17470 mrieqvlemd 17560 cnvps 18518 dirdm 18540 tsrdir 18544 frmdss2 18731 subdrgint 20396 iinopn 22373 neitr 22653 xkococnlem 23132 tgpconncomp 23586 trcfilu 23768 mbfconstlem 25113 itg2seq 25229 limcdif 25362 dvres2lem 25396 c1lip3 25485 lhop 25502 plyeq0 25694 dchrghm 26726 negsbdaylem 27497 precsexlem10 27629 uspgrupgrushgr 28404 upgrreslem 28528 umgrreslem 28529 umgrres1 28538 umgr2v2e 28749 chssoc 30714 gsumhashmul 32179 pmtrcnelor 32223 tocycfvres1 32240 tocycfvres2 32241 dimkerim 32650 hauseqcn 32809 carsgclctunlem3 33250 cvmliftmolem1 34203 cvmlift2lem9a 34225 cvmlift2lem9 34233 cnres2 36537 rngunsnply 41786 proot1hash 41813 omabs2 41953 clcnvlem 42245 cnvtrcl0 42248 trrelsuperrel2dg 42293 brtrclfv2 42349 imo72b2lem1 42792 fourierdlem92 44787 vsetrec 47588 |
Copyright terms: Public domain | W3C validator |