![]() |
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 1893 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) | |
2 | dfcleq 2726 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
3 | dfss2 3968 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
4 | dfss2 3968 | . . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) | |
5 | 3, 4 | anbi12i 628 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
6 | 1, 2, 5 | 3bitr4i 303 | 1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 = wceq 1542 ∈ wcel 2107 ⊆ wss 3948 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3955 df-ss 3965 |
This theorem is referenced by: eqssi 3998 eqssd 3999 sssseq 4000 sseq1 4007 sseq2 4008 ssrabeq 4082 dfpss3 4086 compleq 4147 uneqin 4278 rcompleq 4295 pssdifn0 4365 ss0b 4397 vss 4443 pwpw0 4816 sssn 4829 ssunsn 4831 pwsnOLD 4901 unidif 4946 ssunieq 4947 uniintsn 4991 iuneq1 5013 iuneq2 5016 iunxdif2 5056 ssext 5454 pweqb 5456 eqopab2bw 5548 eqopab2b 5552 pwun 5572 soeq2 5610 eqrel 5783 eqrelrel 5796 coeq1 5856 coeq2 5857 cnveq 5872 dmeq 5902 relssres 6021 xp11 6172 ssrnres 6175 ordtri4 6399 oneqmini 6414 fnres 6675 eqfnfv3 7032 fneqeql2 7046 dff3 7099 fconst4 7213 f1imaeq 7261 eqoprab2bw 7476 eqoprab2b 7477 iunpw 7755 orduniorsuc 7815 tfi 7839 fo1stres 7998 fo2ndres 7999 wfrlem8OLD 8313 tz7.49 8442 oawordeulem 8551 nnacan 8625 nnmcan 8631 ixpeq2 8902 sbthlem3 9082 isinf 9257 isinfOLD 9258 ordunifi 9290 inficl 9417 rankr1c 9813 rankc1 9862 iscard 9967 iscard2 9968 carden2 9979 aleph11 10076 cardaleph 10081 alephinit 10087 dfac12a 10140 cflm 10242 cfslb2n 10260 dfacfin7 10391 wrdeq 14483 isumltss 15791 rpnnen2lem12 16165 isprm2 16616 mrcidb2 17559 smndex2dnrinv 18793 iscyggen2 19744 iscyg3 19749 lssle0 20553 islpir2 20882 iscss2 21231 ishil2 21266 bastop1 22488 epttop 22504 iscld4 22561 0ntr 22567 opnneiid 22622 isperf2 22648 cnntr 22771 ist1-3 22845 perfcls 22861 cmpfi 22904 isconn2 22910 dfconn2 22915 snfil 23360 filconn 23379 ufileu 23415 alexsubALTlem4 23546 metequiv 24010 eqscut2 27297 nbuhgr2vtx1edgblem 28598 iscplgr 28662 shlesb1i 30627 shle0 30683 orthin 30687 chcon2i 30705 chcon3i 30707 chlejb1i 30717 chabs2 30758 h1datomi 30822 cmbr4i 30842 osumcor2i 30885 pjjsi 30941 pjin2i 31434 stcltr2i 31516 mdbr2 31537 dmdbr2 31544 mdsl2i 31563 mdsl2bi 31564 mdslmd3i 31573 chrelat4i 31614 sumdmdlem2 31660 dmdbr5ati 31663 eqdif 31745 eqrelrd2 31833 rspsnasso 32481 dfon2lem9 34752 idsset 34851 fneval 35226 topdifinfeq 36220 equivtotbnd 36635 heiborlem10 36677 eqrel2 37157 relcnveq3 37179 relcnveq2 37181 cossssid 37326 elrelscnveq3 37350 elrelscnveq2 37352 pmap11 38622 dia11N 39908 dia2dimlem5 39928 dib11N 40020 dih11 40125 dihglblem6 40200 doch11 40233 mapd11 40499 mapdcnv11N 40519 sticksstones11 40961 isnacs2 41430 mrefg3 41432 onsupneqmaxlim0 41959 onsupnmax 41963 ontric3g 42259 rababg 42311 relnonrel 42324 uneqsn 42762 ntrk1k3eqk13 42787 ntrneineine1lem 42821 ntrneicls00 42826 ntrneixb 42832 ntrneik13 42835 ntrneix13 42836 joindm2 47555 meetdm2 47557 |
Copyright terms: Public domain | W3C validator |