![]() |
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 3659 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1523 ⊆ wss 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-in 3614 df-ss 3621 |
This theorem is referenced by: eqsstri 3668 syl5eqss 3682 ssab 3705 rabss 3712 uniiunlem 3724 prssg 4382 prssOLD 4384 sstp 4399 tpss 4400 iunss 4593 pwtr 4951 iunopeqop 5010 pwssun 5049 cores2 5686 sspred 5726 dffun2 5936 sbcfg 6081 idref 6539 ovmptss 7303 fnsuppres 7367 ordgt0ge1 7622 omopthlem1 7780 trcl 8642 rankbnd 8769 rankbnd2 8770 rankc1 8771 dfac12a 9008 fin23lem34 9206 axdc2lem 9308 alephval2 9432 indpi 9767 fsuppmapnn0fiublem 12829 0ram 15771 mreacs 16366 lsslinds 20218 2ndcctbss 21306 xkoinjcn 21538 restmetu 22422 xrlimcnp 24740 mptelee 25820 ausgrusgrb 26105 nbuhgr2vtx1edgblem 26292 nbgrsym 26308 nbgrsymOLD 26309 isuvtx 26343 isuvtxaOLD 26344 2wlkdlem6 26896 frcond1 27246 n4cyclfrgr 27271 shlesb1i 28373 mdsldmd1i 29318 csmdsymi 29321 dfon2lem3 31814 dfon2lem7 31818 trpredmintr 31855 filnetlem4 32501 ptrecube 33539 poimirlem30 33569 idinxpssinxp2 34230 cossssid2 34358 symrefref2 34447 undmrnresiss 38227 clcnvlem 38247 ss2iundf 38268 cnvtrrel 38279 brtrclfv2 38336 rp-imass 38382 dfhe3 38386 dffrege76 38550 iunssf 39577 ssabf 39594 rabssf 39616 imassmpt 39795 setrec2 42767 |
Copyright terms: Public domain | W3C validator |