![]() |
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 4005 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1534 ⊆ wss 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-ss 3963 |
This theorem is referenced by: sseqtri 4015 sseqtrdi 4029 abss 4056 ssrab 4066 ssindif0 4458 difcom 4483 ssunsn2 4826 ssunpr 4833 sspr 4834 sstp 4835 ssintrab 4971 iunpwss 5107 propssopi 5506 dffun2OLDOLD 6558 ssimaex 6979 elpwun 7769 ssfi 9204 frfi 9315 alephislim 10119 cardaleph 10125 fin1a2lem12 10445 zornn0g 10539 ssxr 11324 nnwo 12943 isstruct 17149 issubmgm 18690 issubm 18788 grpissubg 19136 issubrng 20525 cntzsubrng 20545 islinds 21803 basdif0 22944 tgdif0 22983 cmpsublem 23391 cmpsub 23392 hauscmplem 23398 2ndcctbss 23447 fbncp 23831 cnextfval 24054 eltsms 24125 reconn 24832 cmssmscld 25366 nocvxminlem 27804 nocvxmin 27805 axcontlem3 28897 axcontlem4 28898 umgredg 29071 nbuhgr 29276 uhgrvd00 29468 vtxdginducedm1 29477 chsscon1i 31392 hatomistici 32292 chirredlem4 32323 atabs2i 32332 mdsymlem1 32333 mdsymlem3 32335 mdsymlem6 32338 mdsymlem8 32340 dmdbr5ati 32352 iundifdif 32483 poimir 37367 ismblfin 37375 cossssid2 38179 ntrk0kbimka 43743 ntrclsk3 43774 ntrneicls11 43794 abssf 44750 ssrabf 44752 stoweidlem57 45714 ovnsubadd 46229 ovnovollem3 46315 linccl 47833 lincdifsn 47843 |
Copyright terms: Public domain | W3C validator |