![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > ILE Home > Th. List > eqss | Structured version GIF version |
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqss | ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albiim 1358 | . 2 ⊢ (∀x(x ∈ A ↔ x ∈ B) ↔ (∀x(x ∈ A → x ∈ B) ∧ ∀x(x ∈ B → x ∈ A))) | |
2 | dfcleq 2017 | . 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B)) | |
3 | dfss2 2910 | . . 3 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B)) | |
4 | dfss2 2910 | . . 3 ⊢ (B ⊆ A ↔ ∀x(x ∈ B → x ∈ A)) | |
5 | 3, 4 | anbi12i 436 | . 2 ⊢ ((A ⊆ B ∧ B ⊆ A) ↔ (∀x(x ∈ A → x ∈ B) ∧ ∀x(x ∈ B → x ∈ A))) |
6 | 1, 2, 5 | 3bitr4i 201 | 1 ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 ∀wal 1226 = wceq 1228 ∈ wcel 1375 ⊆ wss 2893 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1316 ax-7 1317 ax-gen 1318 ax-ie1 1364 ax-ie2 1365 ax-8 1377 ax-11 1379 ax-4 1382 ax-17 1401 ax-i9 1405 ax-ial 1410 ax-i5r 1411 ax-ext 2005 |
This theorem depends on definitions: df-bi 110 df-nf 1330 df-sb 1629 df-clab 2010 df-cleq 2016 df-clel 2019 df-in 2900 df-ss 2907 |
This theorem is referenced by: eqssi 2937 eqssd 2938 sseq1 2942 sseq2 2943 eqimss 2973 ssrabeq 3002 dfpss3 3006 uneqin 3164 ss0b 3232 vss 3240 sssnm 3498 unidif 3585 ssunieq 3586 iuneq1 3643 iuneq2 3646 iunxdif2 3678 ssext 3930 pweqb 3932 eqopab2b 3989 pwunim 3996 soeq2 4026 iunpw 4159 ordunisuc2r 4187 tfi 4230 eqrel 4354 eqrelrel 4366 coeq1 4418 coeq2 4419 cnveq 4434 dmeq 4460 relssres 4573 xp11m 4684 xpcanm 4685 xpcan2m 4686 ssrnres 4688 fnres 4939 eqfnfv3 5190 fneqeql2 5199 fconst4m 5304 f1imaeq 5337 eqoprab2b 5484 fo1stresm 5708 fo2ndresm 5709 nnacan 5991 nnmcan 5998 bj-sseq 6387 bdvsn 6447 bdop 6448 bdeq0 6491 bdeqsuc 6492 bj-om 6501 bj-omexALT 6507 |
Copyright terms: Public domain | W3C validator |