Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqsstr3i | Structured version Visualization version GIF version |
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.) |
Ref | Expression |
---|---|
eqsstr3.1 | ⊢ 𝐵 = 𝐴 |
eqsstr3.2 | ⊢ 𝐵 ⊆ 𝐶 |
Ref | Expression |
---|---|
eqsstr3i | ⊢ 𝐴 ⊆ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsstr3.1 | . . 3 ⊢ 𝐵 = 𝐴 | |
2 | 1 | eqcomi 2631 | . 2 ⊢ 𝐴 = 𝐵 |
3 | eqsstr3.2 | . 2 ⊢ 𝐵 ⊆ 𝐶 | |
4 | 2, 3 | eqsstri 3635 | 1 ⊢ 𝐴 ⊆ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 ⊆ wss 3574 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-in 3581 df-ss 3588 |
This theorem is referenced by: inss2 3834 dmv 5341 ofrfval 6905 ofval 6906 ofrval 6907 off 6912 ofres 6913 ofco 6917 dftpos4 7371 smores2 7451 onwf 8693 r0weon 8835 cda1dif 8998 unctb 9027 infmap2 9040 itunitc 9243 axcclem 9279 dfnn3 11034 bcm1k 13102 bcpasc 13108 cotr2 13716 ressbasss 15932 strlemor1OLD 15969 prdsle 16122 prdsless 16123 dprd2da 18441 opsrle 19475 indiscld 20895 leordtval2 21016 fiuncmp 21207 prdstopn 21431 ustneism 22027 itg1addlem4 23466 itg1addlem5 23467 tdeglem4 23820 aannenlem3 24085 efifo 24293 advlogexp 24401 konigsbergssiedgw 27111 pjoml4i 28446 5oai 28520 3oai 28527 bdopssadj 28940 xrge00 29686 xrge0mulc1cn 29987 esumdivc 30145 ballotlemodife 30559 rpsqrtcn 30671 subfacp1lem5 31166 filnetlem3 32375 filnetlem4 32376 mblfinlem4 33449 itg2gt0cn 33465 psubspset 35030 psubclsetN 35222 relexpaddss 38010 corcltrcl 38031 relopabVD 39137 cncfiooicc 40107 stoweidlem34 40251 amgmwlem 42548 |
Copyright terms: Public domain | W3C validator |