| 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 3949 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
| 4 | 1, 2, 3 | mpbir2an 711 | 1 ⊢ 𝐴 = 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1541 ⊆ wss 3901 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-9 2123 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-cleq 2728 df-ss 3918 |
| This theorem is referenced by: inv1 4350 unv 4351 intab 4933 intabs 5294 dmv 5871 0ima 6037 cnvrescnv 6153 find 7837 dftpos4 8187 dfom3 9556 dmttrcl 9630 rnttrcl 9631 tc2 9649 tcidm 9653 tc0 9654 rankuni 9775 rankval4 9779 djuunxp 9833 djuun 9838 ackbij1 10147 cfom 10174 fin23lem16 10245 itunitc 10331 inaprc 10747 nqerf 10841 dmrecnq 10879 dmaddsr 10996 dmmulsr 10997 axaddf 11056 axmulf 11057 dfnn2 12158 dfuzi 12583 unirnioo 13365 uzrdgfni 13881 0bits 16366 4sqlem19 16891 ledm 18513 lern 18514 efgsfo 19668 0frgp 19708 indiscld 23035 leordtval2 23156 lecldbas 23163 llyidm 23432 nllyidm 23433 toplly 23434 lly1stc 23440 txuni2 23509 txindis 23578 ust0 24164 qdensere 24713 xrtgioo 24751 zdis 24761 xrhmeo 24900 bndth 24913 ismbf3d 25611 dvef 25940 reeff1o 26413 efifo 26512 dvloglem 26613 logf1o2 26615 bday1 27810 oniso 28267 dfn0s2 28328 bdayn0sf1o 28366 dfnns2 28368 choc1 31402 shsidmi 31459 shsval2i 31462 omlsii 31478 chdmm1i 31552 chj1i 31564 chm0i 31565 shjshsi 31567 span0 31617 spanuni 31619 sshhococi 31621 spansni 31632 pjoml4i 31662 pjrni 31777 shatomistici 32436 sumdmdlem2 32494 rinvf1o 32708 sigapildsys 34319 sxbrsigalem0 34428 dya2iocucvr 34441 sxbrsigalem4 34444 sxbrsiga 34447 ballotth 34695 kur14lem6 35405 mrsubrn 35707 msubrn 35723 filnetlem3 36574 filnetlem4 36575 onint1 36643 oninhaus 36644 bj-rabtr 37131 bj-rabtrAUTO 37133 bj-disj2r 37229 bj-nuliotaALT 37259 bj-idres 37365 icoreunrn 37564 dmsucmap 38652 comptiunov2i 43957 unisnALT 45176 fsumiunss 45831 fourierdlem62 46422 fouriersw 46485 salexct 46588 salgencntex 46597 |
| Copyright terms: Public domain | W3C validator |