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 3990 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-in 3940 df-ss 3949 |
This theorem is referenced by: sseqtri 4000 sseqtrdi 4014 abss 4037 ssrab 4046 ssindif0 4409 difcom 4430 ssunsn2 4752 ssunpr 4757 sspr 4758 sstp 4759 ssintrab 4890 iunpwss 5020 propssopi 5389 dffun2 6358 ssimaex 6741 elpwun 7480 frfi 8751 alephislim 9497 cardaleph 9503 fin1a2lem12 9821 zornn0g 9915 ssxr 10698 nnwo 12301 isstruct 16484 issubm 17956 grpissubg 18237 islinds 20881 basdif0 21489 tgdif0 21528 cmpsublem 21935 cmpsub 21936 hauscmplem 21942 2ndcctbss 21991 fbncp 22375 cnextfval 22598 eltsms 22668 reconn 23363 cmssmscld 23880 axcontlem3 26679 axcontlem4 26680 umgredg 26850 nbuhgr 27052 uhgrvd00 27243 vtxdginducedm1 27252 chsscon1i 29166 hatomistici 30066 chirredlem4 30097 atabs2i 30106 mdsymlem1 30107 mdsymlem3 30109 mdsymlem6 30112 mdsymlem8 30114 dmdbr5ati 30126 iundifdif 30242 nocvxminlem 33144 nocvxmin 33145 poimir 34806 ismblfin 34814 cossssid2 35588 ntrk0kbimka 40267 ntrclsk3 40298 ntrneicls11 40318 abssf 41255 ssrabf 41258 stoweidlem57 42219 ovnsubadd 42731 ovnovollem3 42817 issubmgm 43933 linccl 44397 lincdifsn 44407 |
Copyright terms: Public domain | W3C validator |