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 3941 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
4 | 1, 2, 3 | mpbir2an 708 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ⊆ wss 3892 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1545 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-v 3433 df-in 3899 df-ss 3909 |
This theorem is referenced by: inv1 4334 unv 4335 intab 4915 intabs 5270 intid 5377 dmv 5830 0ima 5985 cnvrescnv 6097 find 7737 findOLD 7738 dftpos4 8052 wfrlem16OLD 8146 dfom3 9383 dmttrcl 9457 rnttrcl 9458 tc2 9500 tcidm 9504 tc0 9505 rankuni 9622 rankval4 9626 djuunxp 9680 djuun 9685 ackbij1 9995 cfom 10021 fin23lem16 10092 itunitc 10178 inaprc 10593 nqerf 10687 dmrecnq 10725 dmaddsr 10842 dmmulsr 10843 axaddf 10902 axmulf 10903 dfnn2 11986 dfuzi 12411 unirnioo 13180 uzrdgfni 13676 0bits 16144 4sqlem19 16662 ledm 18306 lern 18307 efgsfo 19343 0frgp 19383 indiscld 22240 leordtval2 22361 lecldbas 22368 llyidm 22637 nllyidm 22638 toplly 22639 lly1stc 22645 txuni2 22714 txindis 22783 ust0 23369 qdensere 23931 xrtgioo 23967 zdis 23977 xrhmeo 24107 bndth 24119 ismbf3d 24816 dvef 25142 reeff1o 25604 efifo 25701 dvloglem 25801 logf1o2 25803 choc1 29685 shsidmi 29742 shsval2i 29745 omlsii 29761 chdmm1i 29835 chj1i 29847 chm0i 29848 shjshsi 29850 span0 29900 spanuni 29902 sshhococi 29904 spansni 29915 pjoml4i 29945 pjrni 30060 shatomistici 30719 sumdmdlem2 30777 rinvf1o 30961 sigapildsys 32126 sxbrsigalem0 32234 dya2iocucvr 32247 sxbrsigalem4 32250 sxbrsiga 32253 ballotth 32500 kur14lem6 33169 mrsubrn 33471 msubrn 33487 bday1s 34021 filnetlem3 34565 filnetlem4 34566 onint1 34634 oninhaus 34635 bj-rabtr 35114 bj-rabtrAUTO 35116 bj-disj2r 35214 bj-nuliotaALT 35225 bj-idres 35327 icoreunrn 35526 comptiunov2i 41284 unisnALT 42516 fsumiunss 43087 fourierdlem62 43680 fouriersw 43743 salexct 43844 salgencntex 43853 |
Copyright terms: Public domain | W3C validator |