| 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 2746 | . 2 ⊢ 𝐴 = 𝐵 |
| 3 | eqsstrrid.2 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | |
| 4 | 2, 3 | eqsstrid 4022 | 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: 3sstr3g 4036 relcnvtrg 6286 fimacnvdisj 6786 dffv2 7004 f1ompt 7131 abnexg 7776 fnwelem 8156 tfrlem15 8432 omxpenlem 9113 hartogslem1 9582 ttrcltr 9756 dfttrcl2 9764 infxpidm2 10057 alephgeom 10122 infenaleph 10131 cfflb 10299 pwfseqlem5 10703 imasvscafn 17582 mrieqvlemd 17672 cnvps 18623 dirdm 18645 tsrdir 18649 frmdss2 18876 subdrgint 20804 iinopn 22908 neitr 23188 xkococnlem 23667 tgpconncomp 24121 trcfilu 24303 mbfconstlem 25662 itg2seq 25777 limcdif 25911 dvres2lem 25945 c1lip3 26038 lhop 26055 plyeq0 26250 dchrghm 27300 negsbdaylem 28088 precsexlem10 28240 uspgrupgrushgr 29196 upgrreslem 29321 umgrreslem 29322 umgrres1 29331 umgr2v2e 29543 chssoc 31515 gsumhashmul 33064 pmtrcnelor 33111 tocycfvres1 33130 tocycfvres2 33131 elrgspnsubrunlem2 33252 dimkerim 33678 hauseqcn 33897 carsgclctunlem3 34322 cvmliftmolem1 35286 cvmlift2lem9a 35308 cvmlift2lem9 35316 cnres2 37770 rngunsnply 43181 proot1hash 43207 omabs2 43345 clcnvlem 43636 cnvtrcl0 43639 trrelsuperrel2dg 43684 brtrclfv2 43740 imo72b2lem1 44182 fourierdlem92 46213 vsetrec 49222 |
| Copyright terms: Public domain | W3C validator |