![]() |
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 3836 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 701 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 ⊆ wss 3792 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-in 3799 df-ss 3806 |
This theorem is referenced by: inv1 4196 unv 4197 intab 4742 intabs 5061 intid 5160 dmv 5588 0ima 5738 find 7371 dftpos4 7655 wfrlem16 7715 dfom3 8843 tc2 8917 tcidm 8921 tc0 8922 rankuni 9025 rankval4 9029 djuunxp 9082 djuun 9087 ackbij1 9397 cfom 9423 fin23lem16 9494 itunitc 9580 inaprc 9995 nqerf 10089 dmrecnq 10127 dmaddsr 10244 dmmulsr 10245 axaddf 10304 axmulf 10305 dfnn2 11394 dfuzi 11825 unirnioo 12591 uzrdgfni 13081 0bits 15577 4sqlem19 16082 ledm 17621 lern 17622 efgsfo 18548 0frgp 18589 indiscld 21314 leordtval2 21435 lecldbas 21442 llyidm 21711 nllyidm 21712 toplly 21713 lly1stc 21719 txuni2 21788 txindis 21857 ust0 22442 qdensere 22992 xrtgioo 23028 zdis 23038 xrhmeo 23164 bndth 23176 ismbf3d 23869 dvef 24191 reeff1o 24649 efifo 24742 dvloglem 24842 logf1o2 24844 choc1 28775 shsidmi 28832 shsval2i 28835 omlsii 28851 chdmm1i 28925 chj1i 28937 chm0i 28938 shjshsi 28940 span0 28990 spanuni 28992 sshhococi 28994 spansni 29005 pjoml4i 29035 pjrni 29150 shatomistici 29809 sumdmdlem2 29867 rinvf1o 30014 sigapildsys 30831 sxbrsigalem0 30939 dya2iocucvr 30952 sxbrsigalem4 30955 sxbrsiga 30958 ballotth 31206 kur14lem6 31800 mrsubrn 32017 msubrn 32033 filnetlem3 32971 filnetlem4 32972 onint1 33039 oninhaus 33040 bj-rabtr 33508 bj-rabtrAUTO 33510 bj-disj2r 33593 bj-nuliotaALT 33600 icoreunrn 33809 comptiunov2i 38969 compneOLD 39613 unisnALT 40109 fsumiunss 40729 fourierdlem62 41326 fouriersw 41389 salexct 41490 salgencntex 41499 |
Copyright terms: Public domain | W3C validator |