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 3979 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 707 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-in 3940 df-ss 3949 |
This theorem is referenced by: inv1 4345 unv 4346 intab 4897 intabs 5236 intid 5341 dmv 5785 0ima 5939 cnvrescnv 6045 find 7596 dftpos4 7900 wfrlem16 7959 dfom3 9098 tc2 9172 tcidm 9176 tc0 9177 rankuni 9280 rankval4 9284 djuunxp 9338 djuun 9343 ackbij1 9648 cfom 9674 fin23lem16 9745 itunitc 9831 inaprc 10246 nqerf 10340 dmrecnq 10378 dmaddsr 10495 dmmulsr 10496 axaddf 10555 axmulf 10556 dfnn2 11639 dfuzi 12061 unirnioo 12825 uzrdgfni 13314 0bits 15776 4sqlem19 16287 ledm 17822 lern 17823 efgsfo 18794 0frgp 18834 indiscld 21627 leordtval2 21748 lecldbas 21755 llyidm 22024 nllyidm 22025 toplly 22026 lly1stc 22032 txuni2 22101 txindis 22170 ust0 22755 qdensere 23305 xrtgioo 23341 zdis 23351 xrhmeo 23477 bndth 23489 ismbf3d 24182 dvef 24504 reeff1o 24962 efifo 25058 dvloglem 25158 logf1o2 25160 choc1 29031 shsidmi 29088 shsval2i 29091 omlsii 29107 chdmm1i 29181 chj1i 29193 chm0i 29194 shjshsi 29196 span0 29246 spanuni 29248 sshhococi 29250 spansni 29261 pjoml4i 29291 pjrni 29406 shatomistici 30065 sumdmdlem2 30123 rinvf1o 30303 sigapildsys 31320 sxbrsigalem0 31428 dya2iocucvr 31441 sxbrsigalem4 31444 sxbrsiga 31447 ballotth 31694 kur14lem6 32355 mrsubrn 32657 msubrn 32673 filnetlem3 33625 filnetlem4 33626 onint1 33694 oninhaus 33695 bj-rabtr 34145 bj-rabtrAUTO 34147 bj-disj2r 34237 bj-nuliotaALT 34245 bj-idres 34344 icoreunrn 34522 comptiunov2i 39929 unisnALT 41137 fsumiunss 41732 fourierdlem62 42330 fouriersw 42393 salexct 42494 salgencntex 42503 |
Copyright terms: Public domain | W3C validator |