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 3590 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 |
This theorem is referenced by: sseqtri 3600 syl6sseq 3614 abss 3634 ssrab 3643 ssindif0 3983 difcom 4005 ssunsn2 4299 ssunpr 4305 sspr 4306 sstp 4307 ssintrab 4435 iunpwss 4551 propssopi 4896 dffun2 5814 ssimaex 6173 elpwun 6869 frfi 8090 alephislim 8789 cardaleph 8795 fin1a2lem12 9116 zornn0g 9210 ssxr 9986 nnwo 11629 isstruct 15705 issubm 17170 grpissubg 17437 islinds 19967 basdif0 20568 tgdif0 20607 cmpsublem 21012 cmpsub 21013 hauscmplem 21019 2ndcctbss 21068 fbncp 21453 cnextfval 21676 eltsms 21746 reconn 22439 axcontlem3 25646 axcontlem4 25647 umgredg 25812 chsscon1i 27705 hatomistici 28605 chirredlem4 28636 atabs2i 28645 mdsymlem1 28646 mdsymlem3 28648 mdsymlem6 28651 mdsymlem8 28653 dmdbr5ati 28665 iundifdif 28763 nocvxminlem 31089 nocvxmin 31090 poimir 32612 ismblfin 32620 ntrk0kbimka 37357 ntrclsk3 37388 ntrneicls11 37408 abssf 38326 ssrabf 38329 stoweidlem57 38950 ovnsubadd 39462 ovnovollem3 39548 nbuhgr 40565 uhgrvd00 40750 issubmgm 41579 linccl 41997 lincdifsn 42007 |
Copyright terms: Public domain | W3C validator |