![]() |
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 4005 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = 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: eqsstri 4014 eqsstrid 4028 ssab 4056 rabss 4067 uniiunlem 4082 prssg 4820 sstp 4835 tpss 4836 iunssf 5045 iunss 5046 pwtr 5450 iunopeqop 5519 pwssun 5569 cores2 6254 resssxp 6265 sspred 6305 dffun2OLDOLD 6551 sbcfg 6711 idref 7138 ovmptss 8073 fnsuppres 8170 frrlem7 8271 ordgt0ge1 8487 omopthlem1 8653 naddasslem1 8688 naddasslem2 8689 dmttrcl 9711 trcl 9718 rankbnd 9858 rankbnd2 9859 rankc1 9860 dfac12a 10138 fin23lem34 10336 axdc2lem 10438 alephval2 10562 indpi 10897 fsuppmapnn0fiublem 13950 0ram 16948 mreacs 17597 lsslinds 21369 2ndcctbss 22940 xkoinjcn 23172 restmetu 24060 xrlimcnp 26452 mptelee 28132 ausgrusgrb 28404 nbuhgr2vtx1edgblem 28587 nbgrsym 28599 isuvtx 28631 2wlkdlem6 29164 frcond1 29498 n4cyclfrgr 29523 shlesb1i 30616 mdsldmd1i 31561 csmdsymi 31564 lfuhgr 34045 2cycl2d 34067 dfon2lem3 34694 dfon2lem7 34698 filnetlem4 35203 ptrecube 36425 poimirlem30 36455 idinxpssinxp2 37124 cossssid2 37275 symrefref2 37370 redundeq1 37436 funALTVfun 37505 disjxrn 37553 omabs2 42014 undmrnresiss 42287 clcnvlem 42306 cnvtrrel 42353 brtrclfv2 42410 dfhe3 42458 dffrege76 42622 mnurndlem1 42972 ssabf 43721 rabssf 43740 imassmpt 43901 setrec2 47641 |
Copyright terms: Public domain | W3C validator |