![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqimss | GIF version |
Description: Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
Ref | Expression |
---|---|
eqimss | ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqss 3025 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
2 | 1 | simplbi 268 | 1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 ⊆ wss 2984 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-11 1438 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-in 2990 df-ss 2997 |
This theorem is referenced by: eqimss2 3063 uneqin 3233 sssnr 3571 sssnm 3572 ssprr 3574 sstpr 3575 snsspw 3582 elpwuni 3788 disjeq2 3796 disjeq1 3799 pwne 3960 pwssunim 4074 poeq2 4090 seeq1 4129 seeq2 4130 trsucss 4213 onsucelsucr 4287 xp11m 4822 funeq 4987 fnresdm 5075 fssxp 5126 ffdm 5129 fcoi1 5138 fof 5180 dff1o2 5205 fvmptss2 5323 fvmptssdm 5331 fprg 5421 dff1o6 5494 tposeq 5943 nntri1 6188 nntri2or2 6190 nnsseleq 6193 infnninf 8643 frec2uzf1od 9701 hashinfuni 10019 |
Copyright terms: Public domain | W3C validator |