![]() |
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 2806 | . 2 ⊢ 𝐴 = 𝐵 |
3 | eqsstr3.2 | . 2 ⊢ 𝐵 ⊆ 𝐶 | |
4 | 2, 3 | eqsstri 3829 | 1 ⊢ 𝐴 ⊆ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 ⊆ wss 3767 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2784 df-cleq 2790 df-clel 2793 df-in 3774 df-ss 3781 |
This theorem is referenced by: inss2 4027 dmv 5542 idssxp 5671 ofrfval 7137 ofval 7138 ofrval 7139 off 7144 ofres 7145 ofco 7149 dftpos4 7607 smores2 7688 onwf 8941 r0weon 9119 cda1dif 9284 unctb 9313 infmap2 9326 itunitc 9529 axcclem 9565 dfnn3 11326 cotr2 14056 ressbasss 16254 prdsle 16434 prdsless 16435 dprd2da 18754 opsrle 19795 indiscld 21221 leordtval2 21342 fiuncmp 21533 prdstopn 21757 ustneism 22352 itg1addlem4 23804 itg1addlem5 23805 tdeglem4 24158 aannenlem3 24423 efifo 24632 konigsbergssiedgw 27589 pjoml4i 28963 5oai 29037 3oai 29044 bdopssadj 29457 xrge00 30194 xrge0mulc1cn 30495 esumdivc 30653 rpsqrtcn 31183 subfacp1lem5 31675 filnetlem3 32879 filnetlem4 32880 mblfinlem4 33930 itg2gt0cn 33945 psubspset 35757 psubclsetN 35949 relexpaddss 38781 corcltrcl 38802 relopabVD 39885 cncfiooicc 40839 amgmwlem 43338 |
Copyright terms: Public domain | W3C validator |