![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sseq2i | Structured version Visualization version GIF version |
Description: An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
sseq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
sseq2i | ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | sseq2 3823 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1653 ⊆ wss 3769 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-in 3776 df-ss 3783 |
This theorem is referenced by: sseqtri 3833 syl6sseq 3847 abss 3867 ssrab 3876 ssindif0 4226 difcom 4247 ssunsn2 4546 ssunpr 4551 sspr 4552 sstp 4553 ssintrab 4690 iunpwss 4809 propssopi 5164 dffun2 6111 ssimaex 6488 elpwun 7211 frfi 8447 alephislim 9192 cardaleph 9198 fin1a2lem12 9521 zornn0g 9615 ssxr 10397 nnwo 11998 isstruct 16197 issubm 17662 grpissubg 17927 islinds 20473 basdif0 21086 tgdif0 21125 cmpsublem 21531 cmpsub 21532 hauscmplem 21538 2ndcctbss 21587 fbncp 21971 cnextfval 22194 eltsms 22264 reconn 22959 cmssmscld 23476 axcontlem3 26203 axcontlem4 26204 umgredg 26374 nbuhgr 26581 uhgrvd00 26784 vtxdginducedm1 26793 chsscon1i 28846 hatomistici 29746 chirredlem4 29777 atabs2i 29786 mdsymlem1 29787 mdsymlem3 29789 mdsymlem6 29792 mdsymlem8 29794 dmdbr5ati 29806 iundifdif 29898 nocvxminlem 32406 nocvxmin 32407 poimir 33931 ismblfin 33939 cossssid2 34712 ntrk0kbimka 39119 ntrclsk3 39150 ntrneicls11 39170 abssf 40053 ssrabf 40056 stoweidlem57 41017 ovnsubadd 41532 ovnovollem3 41618 issubmgm 42588 linccl 43002 lincdifsn 43012 |
Copyright terms: Public domain | W3C validator |