Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqss | GIF version |
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqss | ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albiim 1480 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) | |
2 | dfcleq 2164 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
3 | dfss2 3136 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
4 | dfss2 3136 | . . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) | |
5 | 3, 4 | anbi12i 457 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) |
6 | 1, 2, 5 | 3bitr4i 211 | 1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1346 = wceq 1348 ∈ wcel 2141 ⊆ wss 3121 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-in 3127 df-ss 3134 |
This theorem is referenced by: eqssi 3163 eqssd 3164 sseq1 3170 sseq2 3171 eqimss 3201 ssrabeq 3234 uneqin 3378 ss0b 3454 vss 3462 sssnm 3741 unidif 3828 ssunieq 3829 iuneq1 3886 iuneq2 3889 iunxdif2 3921 ssext 4206 pweqb 4208 eqopab2b 4264 pwunim 4271 soeq2 4301 iunpw 4465 ordunisuc2r 4498 tfi 4566 eqrel 4700 eqrelrel 4712 coeq1 4768 coeq2 4769 cnveq 4785 dmeq 4811 relssres 4929 xp11m 5049 xpcanm 5050 xpcan2m 5051 ssrnres 5053 fnres 5314 eqfnfv3 5595 fneqeql2 5605 fconst4m 5716 f1imaeq 5754 eqoprab2b 5911 fo1stresm 6140 fo2ndresm 6141 nnacan 6491 nnmcan 6498 ixpeq2 6690 sbthlemi3 6936 isprm2 12071 bastop1 12877 epttop 12884 opnneiid 12958 cnntr 13019 metequiv 13289 bj-sseq 13827 bdeq0 13902 bdvsn 13909 bdop 13910 bdeqsuc 13916 bj-om 13972 |
Copyright terms: Public domain | W3C validator |