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 1897 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) | |
2 | dfcleq 2730 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
3 | dfss2 3883 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
4 | dfss2 3883 | . . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) | |
5 | 3, 4 | anbi12i 630 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
6 | 1, 2, 5 | 3bitr4i 306 | 1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∀wal 1541 = wceq 1543 ∈ wcel 2110 ⊆ wss 3863 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3407 df-in 3870 df-ss 3880 |
This theorem is referenced by: eqssi 3914 eqssd 3915 sssseq 3916 sseq1 3923 sseq2 3924 eqimss 3954 ssrabeq 3994 dfpss3 3998 compleq 4059 uneqin 4190 rcompleq 4207 pssdifn0 4277 ss0b 4309 vss 4355 pwpw0 4723 sssn 4736 ssunsn 4738 pwsnOLD 4809 unidif 4852 ssunieq 4853 uniintsn 4895 iuneq1 4917 iuneq2 4920 iunxdif2 4959 ssext 5336 pweqb 5338 eqopab2bw 5426 eqopab2b 5430 pwun 5450 soeq2 5487 eqrel 5652 eqrelrel 5664 coeq1 5723 coeq2 5724 cnveq 5739 dmeq 5769 relssres 5889 xp11 6035 ssrnres 6038 ordtri4 6247 oneqmini 6261 fnres 6501 eqfnfv3 6851 fneqeql2 6864 dff3 6916 fconst4 7027 f1imaeq 7074 eqoprab2bw 7278 eqoprab2b 7279 iunpw 7553 orduniorsuc 7606 tfi 7629 fo1stres 7784 fo2ndres 7785 wfrlem8 8059 tz7.49 8178 oawordeulem 8279 nnacan 8353 nnmcan 8359 ixpeq2 8589 sbthlem3 8755 isinf 8888 ordunifi 8918 inficl 9038 rankr1c 9434 rankc1 9483 iscard 9588 iscard2 9589 carden2 9600 aleph11 9695 cardaleph 9700 alephinit 9706 dfac12a 9759 cflm 9861 cfslb2n 9879 dfacfin7 10010 wrdeq 14088 isumltss 15409 rpnnen2lem12 15783 isprm2 16236 mrcidb2 17118 smndex2dnrinv 18339 iscyggen2 19262 iscyg3 19267 lssle0 19983 islpir2 20286 iscss2 20645 ishil2 20678 bastop1 21887 epttop 21903 iscld4 21959 0ntr 21965 opnneiid 22020 isperf2 22046 cnntr 22169 ist1-3 22243 perfcls 22259 cmpfi 22302 isconn2 22308 dfconn2 22313 snfil 22758 filconn 22777 ufileu 22813 alexsubALTlem4 22944 metequiv 23404 nbuhgr2vtx1edgblem 27436 iscplgr 27500 shlesb1i 29464 shle0 29520 orthin 29524 chcon2i 29542 chcon3i 29544 chlejb1i 29554 chabs2 29595 h1datomi 29659 cmbr4i 29679 osumcor2i 29722 pjjsi 29778 pjin2i 30271 stcltr2i 30353 mdbr2 30374 dmdbr2 30381 mdsl2i 30400 mdsl2bi 30401 mdslmd3i 30410 chrelat4i 30451 sumdmdlem2 30497 dmdbr5ati 30500 eqdif 30582 eqrelrd2 30672 dfon2lem9 33483 eqscut2 33734 idsset 33926 fneval 34275 topdifinfeq 35255 equivtotbnd 35671 heiborlem10 35713 eqrel2 36170 relcnveq3 36191 relcnveq2 36193 cossssid 36320 elrelscnveq3 36344 elrelscnveq2 36346 pmap11 37511 dia11N 38797 dia2dimlem5 38817 dib11N 38909 dih11 39014 dihglblem6 39089 doch11 39122 mapd11 39388 mapdcnv11N 39408 sticksstones11 39832 isnacs2 40229 mrefg3 40231 ontric3g 40812 rababg 40855 relnonrel 40869 uneqsn 41308 ntrk1k3eqk13 41335 ntrneineine1lem 41369 ntrneicls00 41374 ntrneixb 41380 ntrneik13 41383 ntrneix13 41384 joindm2 45933 meetdm2 45935 |
Copyright terms: Public domain | W3C validator |