![]() |
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 3920 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1525 ⊆ wss 3865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-in 3872 df-ss 3880 |
This theorem is referenced by: sseqtri 3930 syl6sseq 3944 abss 3967 ssrab 3976 ssindif0 4333 difcom 4354 ssunsn2 4673 ssunpr 4678 sspr 4679 sstp 4680 ssintrab 4811 iunpwss 4934 propssopi 5296 dffun2 6242 ssimaex 6622 elpwun 7355 frfi 8616 alephislim 9362 cardaleph 9368 fin1a2lem12 9686 zornn0g 9780 ssxr 10563 nnwo 12166 isstruct 16329 issubm 17790 grpissubg 18057 islinds 20639 basdif0 21249 tgdif0 21288 cmpsublem 21695 cmpsub 21696 hauscmplem 21702 2ndcctbss 21751 fbncp 22135 cnextfval 22358 eltsms 22428 reconn 23123 cmssmscld 23640 axcontlem3 26439 axcontlem4 26440 umgredg 26610 nbuhgr 26812 uhgrvd00 27003 vtxdginducedm1 27012 chsscon1i 28926 hatomistici 29826 chirredlem4 29857 atabs2i 29866 mdsymlem1 29867 mdsymlem3 29869 mdsymlem6 29872 mdsymlem8 29874 dmdbr5ati 29886 iundifdif 30000 nocvxminlem 32858 nocvxmin 32859 poimir 34477 ismblfin 34485 cossssid2 35260 ntrk0kbimka 39895 ntrclsk3 39926 ntrneicls11 39946 abssf 40939 ssrabf 40942 stoweidlem57 41906 ovnsubadd 42418 ovnovollem3 42504 issubmgm 43560 linccl 43971 lincdifsn 43981 |
Copyright terms: Public domain | W3C validator |