Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqssi | Structured version Visualization version GIF version |
Description: Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.) |
Ref | Expression |
---|---|
eqssi.1 | ⊢ 𝐴 ⊆ 𝐵 |
eqssi.2 | ⊢ 𝐵 ⊆ 𝐴 |
Ref | Expression |
---|---|
eqssi | ⊢ 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqssi.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | eqssi.2 | . 2 ⊢ 𝐵 ⊆ 𝐴 | |
3 | eqss 3618 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 955 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 ⊆ wss 3574 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-in 3581 df-ss 3588 |
This theorem is referenced by: inv1 3970 unv 3971 intab 4507 intabs 4825 intid 4926 dmv 5341 0ima 5482 fresaunres2 6076 find 7091 dftpos4 7371 wfrlem16 7430 dfom3 8544 tc2 8618 tcidm 8622 tc0 8623 rankuni 8726 rankval4 8730 ackbij1 9060 cfom 9086 fin23lem16 9157 itunitc 9243 inaprc 9658 nqerf 9752 dmrecnq 9790 dmaddsr 9906 dmmulsr 9907 axaddf 9966 axmulf 9967 dfnn2 11033 dfuzi 11468 unirnioo 12273 uzrdgfni 12757 0bits 15161 4sqlem19 15667 ledm 17224 lern 17225 efgsfo 18152 0frgp 18192 indiscld 20895 leordtval2 21016 lecldbas 21023 llyidm 21291 nllyidm 21292 toplly 21293 lly1stc 21299 txuni2 21368 txindis 21437 ust0 22023 qdensere 22573 xrtgioo 22609 zdis 22619 xrhmeo 22745 bndth 22757 ismbf3d 23421 dvef 23743 reeff1o 24201 efifo 24293 dvloglem 24394 logf1o2 24396 choc1 28186 shsidmi 28243 shsval2i 28246 omlsii 28262 chdmm1i 28336 chj1i 28348 chm0i 28349 shjshsi 28351 span0 28401 spanuni 28403 sshhococi 28405 spansni 28416 pjoml4i 28446 pjrni 28561 shatomistici 29220 sumdmdlem2 29278 rinvf1o 29432 sigapildsys 30225 sxbrsigalem0 30333 dya2iocucvr 30346 sxbrsigalem4 30349 sxbrsiga 30352 ballotth 30599 kur14lem6 31193 mrsubrn 31410 msubrn 31426 filnetlem3 32375 filnetlem4 32376 onint1 32448 oninhaus 32449 bj-rabtr 32926 bj-rabtrALTALT 32928 bj-rabtrAUTO 32929 bj-disj2r 33013 bj-nuliotaALT 33020 icoreunrn 33207 idinxpres 34088 comptiunov2i 37998 compneOLD 38644 unisnALT 39162 fsumiunss 39807 fourierdlem62 40385 fouriersw 40448 salexct 40552 salgencntex 40561 |
Copyright terms: Public domain | W3C validator |