| 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 4010 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 |
| This theorem is referenced by: sseqtrdi 4024 sseqtri 4032 abss 4063 ssrab 4073 ssindif0 4464 difcom 4489 ssunsn2 4827 ssunpr 4834 sspr 4835 sstp 4836 ssintrab 4971 iunpwss 5107 propssopi 5513 dffun2OLDOLD 6573 f1imadifssran 6652 ssimaex 6994 elpwun 7789 ssfi 9213 frfi 9321 alephislim 10123 cardaleph 10129 fin1a2lem12 10451 zornn0g 10545 ssxr 11330 nnwo 12955 isstruct 17189 issubmgm 18715 issubm 18816 grpissubg 19164 issubrng 20547 cntzsubrng 20567 islinds 21829 basdif0 22960 tgdif0 22999 cmpsublem 23407 cmpsub 23408 hauscmplem 23414 2ndcctbss 23463 fbncp 23847 cnextfval 24070 eltsms 24141 reconn 24850 cmssmscld 25384 nocvxminlem 27822 nocvxmin 27823 axcontlem3 28981 axcontlem4 28982 umgredg 29155 nbuhgr 29360 uhgrvd00 29552 vtxdginducedm1 29561 chsscon1i 31481 hatomistici 32381 chirredlem4 32412 atabs2i 32421 mdsymlem1 32422 mdsymlem3 32424 mdsymlem6 32427 mdsymlem8 32429 dmdbr5ati 32441 iundifdif 32575 poimir 37660 ismblfin 37668 cossssid2 38469 ntrk0kbimka 44052 ntrclsk3 44083 ntrneicls11 44103 wfaxrep 45011 wfaxsep 45012 abssf 45117 ssrabf 45119 stoweidlem57 46072 ovnsubadd 46587 ovnovollem3 46673 linccl 48331 lincdifsn 48341 |
| Copyright terms: Public domain | W3C validator |