![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqss | Structured version Visualization version GIF version |
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.) |
Ref | Expression |
---|---|
eqss | ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albiim 1856 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) | |
2 | dfcleq 2645 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
3 | dfss2 3624 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
4 | dfss2 3624 | . . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) | |
5 | 3, 4 | anbi12i 733 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
6 | 1, 2, 5 | 3bitr4i 292 | 1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∀wal 1521 = wceq 1523 ∈ wcel 2030 ⊆ wss 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-in 3614 df-ss 3621 |
This theorem is referenced by: eqssi 3652 eqssd 3653 sssseq 3654 sseq1 3659 sseq2 3660 eqimss 3690 ssrabeq 3722 dfpss3 3726 compleq 3785 uneqin 3911 pssdifn0 3977 ss0b 4006 vss 4045 pwpw0 4376 sssn 4390 ssunsn 4392 pwsnALT 4461 unidif 4503 ssunieq 4504 uniintsn 4546 iuneq1 4566 iuneq2 4569 iunxdif2 4600 ssext 4953 pweqb 4955 eqopab2b 5034 pwun 5051 soeq2 5084 eqrel 5243 eqrelrel 5255 coeq1 5312 coeq2 5313 cnveq 5328 dmeq 5356 relssres 5472 xp11 5604 ssrnres 5607 ordtri4 5799 oneqmini 5814 fnres 6045 eqfnfv3 6353 fneqeql2 6366 dff3 6412 fconst4 6519 f1imaeq 6562 eqoprab2b 6755 iunpw 7020 orduniorsuc 7072 tfi 7095 fo1stres 7236 fo2ndres 7237 wfrlem8 7467 tz7.49 7585 oawordeulem 7679 nnacan 7753 nnmcan 7759 ixpeq2 7964 sbthlem3 8113 isinf 8214 ordunifi 8251 inficl 8372 rankr1c 8722 rankc1 8771 iscard 8839 iscard2 8840 carden2 8851 aleph11 8945 cardaleph 8950 alephinit 8956 dfac12a 9008 cflm 9110 cfslb2n 9128 dfacfin7 9259 wrdeq 13359 isumltss 14624 rpnnen2lem12 14998 isprm2 15442 mrcidb2 16325 iscyggen2 18329 iscyg3 18334 lssle0 18998 islpir2 19299 iscss2 20078 ishil2 20111 bastop1 20845 epttop 20861 iscld4 20917 0ntr 20923 opnneiid 20978 isperf2 21004 cnntr 21127 ist1-3 21201 perfcls 21217 cmpfi 21259 isconn2 21265 dfconn2 21270 snfil 21715 filconn 21734 ufileu 21770 alexsubALTlem4 21901 metequiv 22361 nbuhgr2vtx1edgblem 26292 iscplgr 26366 shlesb1i 28373 shle0 28429 orthin 28433 chcon2i 28451 chcon3i 28453 chlejb1i 28463 chabs2 28504 h1datomi 28568 cmbr4i 28588 osumcor2i 28631 pjjsi 28687 pjin2i 29180 stcltr2i 29262 mdbr2 29283 dmdbr2 29290 mdsl2i 29309 mdsl2bi 29310 mdslmd3i 29319 chrelat4i 29360 sumdmdlem2 29406 dmdbr5ati 29409 eqrelrd2 29554 dfon2lem9 31820 idsset 32122 fneval 32472 topdifinfeq 33328 equivtotbnd 33707 heiborlem10 33749 eqrel2 34209 relcnveq3 34233 relcnveq2 34235 cossssid 34357 elrelscnveq3 34381 elrelscnveq2 34383 pmap11 35366 dia11N 36654 dia2dimlem5 36674 dib11N 36766 dih11 36871 dihglblem6 36946 doch11 36979 mapd11 37245 mapdcnv11N 37265 isnacs2 37586 mrefg3 37588 rababg 38196 relnonrel 38210 rcompleq 38635 uneqsn 38638 ntrk1k3eqk13 38665 ntrneineine1lem 38699 ntrneicls00 38704 ntrneixb 38710 ntrneik13 38713 ntrneix13 38714 prsal 40856 |
Copyright terms: Public domain | W3C validator |