![]() |
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 3930 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 710 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 ⊆ wss 3881 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-in 3888 df-ss 3898 |
This theorem is referenced by: inv1 4302 unv 4303 intab 4868 intabs 5209 intid 5315 dmv 5756 0ima 5913 cnvrescnv 6019 find 7587 findOLD 7588 dftpos4 7894 wfrlem16 7953 dfom3 9094 tc2 9168 tcidm 9172 tc0 9173 rankuni 9276 rankval4 9280 djuunxp 9334 djuun 9339 ackbij1 9649 cfom 9675 fin23lem16 9746 itunitc 9832 inaprc 10247 nqerf 10341 dmrecnq 10379 dmaddsr 10496 dmmulsr 10497 axaddf 10556 axmulf 10557 dfnn2 11638 dfuzi 12061 unirnioo 12827 uzrdgfni 13321 0bits 15778 4sqlem19 16289 ledm 17826 lern 17827 efgsfo 18857 0frgp 18897 indiscld 21696 leordtval2 21817 lecldbas 21824 llyidm 22093 nllyidm 22094 toplly 22095 lly1stc 22101 txuni2 22170 txindis 22239 ust0 22825 qdensere 23375 xrtgioo 23411 zdis 23421 xrhmeo 23551 bndth 23563 ismbf3d 24258 dvef 24583 reeff1o 25042 efifo 25139 dvloglem 25239 logf1o2 25241 choc1 29110 shsidmi 29167 shsval2i 29170 omlsii 29186 chdmm1i 29260 chj1i 29272 chm0i 29273 shjshsi 29275 span0 29325 spanuni 29327 sshhococi 29329 spansni 29340 pjoml4i 29370 pjrni 29485 shatomistici 30144 sumdmdlem2 30202 rinvf1o 30389 sigapildsys 31531 sxbrsigalem0 31639 dya2iocucvr 31652 sxbrsigalem4 31655 sxbrsiga 31658 ballotth 31905 kur14lem6 32571 mrsubrn 32873 msubrn 32889 filnetlem3 33841 filnetlem4 33842 onint1 33910 oninhaus 33911 bj-rabtr 34372 bj-rabtrAUTO 34374 bj-disj2r 34464 bj-nuliotaALT 34475 bj-idres 34575 icoreunrn 34776 comptiunov2i 40407 unisnALT 41632 fsumiunss 42217 fourierdlem62 42810 fouriersw 42873 salexct 42974 salgencntex 42983 |
Copyright terms: Public domain | W3C validator |