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 3989 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-in 3940 df-ss 3949 |
This theorem is referenced by: eqsstri 3998 eqsstrid 4012 ssab 4038 rabss 4045 uniiunlem 4058 prssg 4744 sstp 4759 tpss 4760 iunss 4960 pwtr 5336 iunopeqop 5402 pwssun 5448 cores2 6105 sspred 6149 dffun2 6358 sbcfg 6505 idref 6900 ovmptss 7777 fnsuppres 7846 ordgt0ge1 8111 omopthlem1 8271 trcl 9158 rankbnd 9285 rankbnd2 9286 rankc1 9287 dfac12a 9562 fin23lem34 9756 axdc2lem 9858 alephval2 9982 indpi 10317 fsuppmapnn0fiublem 13346 0ram 16344 mreacs 16917 lsslinds 20903 2ndcctbss 21991 xkoinjcn 22223 restmetu 23107 xrlimcnp 25473 mptelee 26608 ausgrusgrb 26877 nbuhgr2vtx1edgblem 27060 nbgrsym 27072 isuvtx 27104 2wlkdlem6 27637 frcond1 27972 n4cyclfrgr 27997 shlesb1i 29090 mdsldmd1i 30035 csmdsymi 30038 lfuhgr 32261 2cycl2d 32283 dfon2lem3 32927 dfon2lem7 32931 trpredmintr 32967 frrlem7 33026 filnetlem4 33626 ptrecube 34773 poimirlem30 34803 idinxpssinxp2 35456 cossssid2 35588 symrefref2 35679 redundeq1 35744 funALTVfun 35811 disjxrn 35857 undmrnresiss 39842 clcnvlem 39861 ss2iundf 39882 cnvtrrel 39893 brtrclfv2 39950 rp-imass 39995 dfhe3 39999 dffrege76 40163 mnurndlem1 40494 iunssf 41229 ssabf 41243 rabssf 41262 imassmpt 41413 setrec2 44726 |
Copyright terms: Public domain | W3C validator |