Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sseq1i | Structured version Visualization version GIF version |
Description: An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.) |
Ref | Expression |
---|---|
sseq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
sseq1i | ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | sseq1 3589 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 |
This theorem is referenced by: eqsstri 3598 syl5eqss 3612 ssab 3635 rabss 3642 uniiunlem 3653 prssg 4290 prssOLD 4292 sstp 4307 tpss 4308 iunss 4497 pwtr 4848 iunopeqop 4906 pwssun 4944 cores2 5565 sspred 5605 dffun2 5814 sbcfg 5956 idref 6403 ovmptss 7145 fnsuppres 7209 ordgt0ge1 7464 omopthlem1 7622 trcl 8487 rankbnd 8614 rankbnd2 8615 rankc1 8616 dfac12a 8853 fin23lem34 9051 axdc2lem 9153 alephval2 9273 indpi 9608 fsuppmapnn0fiublem 12651 0ram 15562 mreacs 16142 lsslinds 19989 2ndcctbss 21068 xkoinjcn 21300 restmetu 22185 xrlimcnp 24495 mptelee 25575 ausisusgra 25884 frgraunss 26522 n4cyclfrgra 26545 shlesb1i 27629 mdsldmd1i 28574 csmdsymi 28577 dfon2lem3 30934 dfon2lem7 30938 trpredmintr 30975 filnetlem4 31546 ptrecube 32579 poimirlem30 32609 undmrnresiss 36929 clcnvlem 36949 ss2iundf 36970 cnvtrrel 36981 brtrclfv2 37038 rp-imass 37085 dfhe3 37089 dffrege76 37253 iunssf 38290 ssabf 38308 rabssf 38334 ausgrusgrb 40395 nbuhgr2vtx1edgblem 40573 nbgrsym 40591 isuvtxa 40621 21wlkdlem6 41138 frcond1 41438 n4cyclfrgr 41461 setrec2 42241 |
Copyright terms: Public domain | W3C validator |