![]() |
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 3775 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1631 ⊆ wss 3723 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-in 3730 df-ss 3737 |
This theorem is referenced by: eqsstri 3784 syl5eqss 3798 ssab 3821 rabss 3828 uniiunlem 3841 prssg 4485 sstp 4500 tpss 4501 iunss 4695 pwtr 5049 iunopeqop 5114 pwssun 5153 cores2 5792 sspred 5831 dffun2 6041 sbcfg 6183 idref 6642 ovmptss 7409 fnsuppres 7474 ordgt0ge1 7731 omopthlem1 7889 trcl 8768 rankbnd 8895 rankbnd2 8896 rankc1 8897 dfac12a 9172 fin23lem34 9370 axdc2lem 9472 alephval2 9596 indpi 9931 fsuppmapnn0fiublem 12997 0ram 15931 mreacs 16526 lsslinds 20387 2ndcctbss 21479 xkoinjcn 21711 restmetu 22595 xrlimcnp 24916 mptelee 25996 ausgrusgrb 26282 nbuhgr2vtx1edgblem 26470 nbgrsym 26486 nbgrsymOLD 26487 isuvtx 26522 isuvtxaOLD 26523 2wlkdlem6 27078 frcond1 27448 n4cyclfrgr 27473 shlesb1i 28585 mdsldmd1i 29530 csmdsymi 29533 dfon2lem3 32026 dfon2lem7 32030 trpredmintr 32067 filnetlem4 32713 ptrecube 33742 poimirlem30 33772 idinxpssinxp2 34432 cossssid2 34560 symrefref2 34651 undmrnresiss 38436 clcnvlem 38456 ss2iundf 38477 cnvtrrel 38488 brtrclfv2 38545 rp-imass 38591 dfhe3 38595 dffrege76 38759 iunssf 39784 ssabf 39801 rabssf 39823 imassmpt 39999 setrec2 42970 |
Copyright terms: Public domain | W3C validator |