| 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 4009 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = 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: eqsstrid 4022 eqsstri 4030 ssab 4064 rabss 4072 uniiunlem 4087 prssg 4819 sstp 4836 tpss 4837 iunssf 5044 iunss 5045 pwtr 5457 iunopeqop 5526 pwssun 5575 imadifssran 6171 cores2 6279 resssxp 6290 sspred 6330 dffun2OLDOLD 6573 sbcfg 6734 idref 7166 ovmptss 8118 fnsuppres 8216 frrlem7 8317 ordgt0ge1 8531 omopthlem1 8697 naddasslem1 8732 naddasslem2 8733 dmttrcl 9761 trcl 9768 rankbnd 9908 rankbnd2 9909 rankc1 9910 dfac12a 10189 fin23lem34 10386 axdc2lem 10488 alephval2 10612 indpi 10947 fsuppmapnn0fiublem 14031 prodeq1i 15952 0ram 17058 mreacs 17701 lsslinds 21851 2ndcctbss 23463 xkoinjcn 23695 restmetu 24583 xrlimcnp 27011 mptelee 28910 ausgrusgrb 29182 nbuhgr2vtx1edgblem 29368 nbgrsym 29380 isuvtx 29412 2wlkdlem6 29951 frcond1 30285 n4cyclfrgr 30310 shlesb1i 31405 mdsldmd1i 32350 csmdsymi 32353 lfuhgr 35123 2cycl2d 35144 dfon2lem3 35786 dfon2lem7 35790 cbvprodvw2 36248 filnetlem4 36382 ptrecube 37627 poimirlem30 37657 idinxpssinxp2 38319 cossssid2 38469 symrefref2 38564 redundeq1 38630 funALTVfun 38699 disjxrn 38747 omabs2 43345 undmrnresiss 43617 clcnvlem 43636 cnvtrrel 43683 brtrclfv2 43740 dfhe3 43788 dffrege76 43952 mnurndlem1 44300 ssabf 45105 rabssf 45124 imassmpt 45269 clnbgrsym 47824 sclnbgrelself 47834 setrec2 49214 |
| Copyright terms: Public domain | W3C validator |