![]() |
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 3759 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 993 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1632 ⊆ wss 3715 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-in 3722 df-ss 3729 |
This theorem is referenced by: inv1 4113 unv 4114 intab 4659 intabs 4974 intid 5075 dmv 5496 0ima 5640 fresaunres2 6237 find 7256 dftpos4 7540 wfrlem16 7599 dfom3 8717 tc2 8791 tcidm 8795 tc0 8796 rankuni 8899 rankval4 8903 djuun 8950 ackbij1 9252 cfom 9278 fin23lem16 9349 itunitc 9435 inaprc 9850 nqerf 9944 dmrecnq 9982 dmaddsr 10098 dmmulsr 10099 axaddf 10158 axmulf 10159 dfnn2 11225 dfuzi 11660 unirnioo 12466 uzrdgfni 12951 0bits 15363 4sqlem19 15869 ledm 17425 lern 17426 efgsfo 18352 0frgp 18392 indiscld 21097 leordtval2 21218 lecldbas 21225 llyidm 21493 nllyidm 21494 toplly 21495 lly1stc 21501 txuni2 21570 txindis 21639 ust0 22224 qdensere 22774 xrtgioo 22810 zdis 22820 xrhmeo 22946 bndth 22958 ismbf3d 23620 dvef 23942 reeff1o 24400 efifo 24492 dvloglem 24593 logf1o2 24595 choc1 28495 shsidmi 28552 shsval2i 28555 omlsii 28571 chdmm1i 28645 chj1i 28657 chm0i 28658 shjshsi 28660 span0 28710 spanuni 28712 sshhococi 28714 spansni 28725 pjoml4i 28755 pjrni 28870 shatomistici 29529 sumdmdlem2 29587 rinvf1o 29741 sigapildsys 30534 sxbrsigalem0 30642 dya2iocucvr 30655 sxbrsigalem4 30658 sxbrsiga 30661 ballotth 30908 kur14lem6 31500 mrsubrn 31717 msubrn 31733 filnetlem3 32681 filnetlem4 32682 onint1 32754 oninhaus 32755 bj-rabtr 33232 bj-rabtrALTALT 33234 bj-rabtrAUTO 33235 bj-disj2r 33319 bj-nuliotaALT 33326 icoreunrn 33518 idinxpres 34412 comptiunov2i 38500 compneOLD 39146 unisnALT 39661 fsumiunss 40310 fourierdlem62 40888 fouriersw 40951 salexct 41055 salgencntex 41064 |
Copyright terms: Public domain | W3C validator |