![]() |
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 2660 | . 2 ⊢ 𝐴 = 𝐵 |
3 | eqsstr3.2 | . 2 ⊢ 𝐵 ⊆ 𝐶 | |
4 | 2, 3 | eqsstri 3668 | 1 ⊢ 𝐴 ⊆ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ⊆ wss 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-in 3614 df-ss 3621 |
This theorem is referenced by: inss2 3867 dmv 5373 ofrfval 6947 ofval 6948 ofrval 6949 off 6954 ofres 6955 ofco 6959 dftpos4 7416 smores2 7496 onwf 8731 r0weon 8873 cda1dif 9036 unctb 9065 infmap2 9078 itunitc 9281 axcclem 9317 dfnn3 11072 cotr2 13762 ressbasss 15979 strlemor1OLD 16016 prdsle 16169 prdsless 16170 dprd2da 18487 opsrle 19523 indiscld 20943 leordtval2 21064 fiuncmp 21255 prdstopn 21479 ustneism 22074 itg1addlem4 23511 itg1addlem5 23512 tdeglem4 23865 aannenlem3 24130 efifo 24338 konigsbergssiedgw 27228 pjoml4i 28574 5oai 28648 3oai 28655 bdopssadj 29068 xrge00 29814 xrge0mulc1cn 30115 esumdivc 30273 rpsqrtcn 30799 subfacp1lem5 31292 filnetlem3 32500 filnetlem4 32501 mblfinlem4 33579 itg2gt0cn 33595 psubspset 35348 psubclsetN 35540 relexpaddss 38327 corcltrcl 38348 relopabVD 39451 cncfiooicc 40425 amgmwlem 42876 |
Copyright terms: Public domain | W3C validator |