![]() |
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 3995 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 709 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ⊆ wss 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-ss 3964 |
This theorem is referenced by: inv1 4399 unv 4400 intab 4988 intabs 5351 intidOLD 5466 dmv 5931 0ima 6089 cnvrescnv 6208 find 7910 dftpos4 8262 wfrlem16OLD 8356 dfom3 9692 dmttrcl 9766 rnttrcl 9767 tc2 9787 tcidm 9791 tc0 9792 rankuni 9908 rankval4 9912 djuunxp 9966 djuun 9971 ackbij1 10283 cfom 10309 fin23lem16 10380 itunitc 10466 inaprc 10881 nqerf 10975 dmrecnq 11013 dmaddsr 11130 dmmulsr 11131 axaddf 11190 axmulf 11191 dfnn2 12279 dfuzi 12707 unirnioo 13482 uzrdgfni 13980 0bits 16441 4sqlem19 16967 ledm 18617 lern 18618 efgsfo 19739 0frgp 19779 indiscld 23089 leordtval2 23210 lecldbas 23217 llyidm 23486 nllyidm 23487 toplly 23488 lly1stc 23494 txuni2 23563 txindis 23632 ust0 24218 qdensere 24780 xrtgioo 24816 zdis 24826 xrhmeo 24965 bndth 24978 ismbf3d 25677 dvef 26006 reeff1o 26480 efifo 26577 dvloglem 26678 logf1o2 26680 bday1s 27864 dfn0s2 28307 choc1 31263 shsidmi 31320 shsval2i 31323 omlsii 31339 chdmm1i 31413 chj1i 31425 chm0i 31426 shjshsi 31428 span0 31478 spanuni 31480 sshhococi 31482 spansni 31493 pjoml4i 31523 pjrni 31638 shatomistici 32297 sumdmdlem2 32355 rinvf1o 32549 sigapildsys 33997 sxbrsigalem0 34107 dya2iocucvr 34120 sxbrsigalem4 34123 sxbrsiga 34126 ballotth 34373 kur14lem6 35041 mrsubrn 35343 msubrn 35359 filnetlem3 36094 filnetlem4 36095 onint1 36163 oninhaus 36164 bj-rabtr 36638 bj-rabtrAUTO 36640 bj-disj2r 36737 bj-nuliotaALT 36767 bj-idres 36869 icoreunrn 37068 comptiunov2i 43391 unisnALT 44620 fsumiunss 45214 fourierdlem62 45807 fouriersw 45870 salexct 45973 salgencntex 45982 |
Copyright terms: Public domain | W3C validator |