| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eqsstrri | 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 |
|---|---|
| eqsstrri | ⊢ 𝐴 ⊆ 𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqsstr3.1 | . . 3 ⊢ 𝐵 = 𝐴 | |
| 2 | 1 | eqcomi 2746 | . 2 ⊢ 𝐴 = 𝐵 |
| 3 | eqsstr3.2 | . 2 ⊢ 𝐵 ⊆ 𝐶 | |
| 4 | 2, 3 | eqsstri 4030 | 1 ⊢ 𝐴 ⊆ 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: = 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: 3sstr3i 4034 inss2 4238 dmv 5933 idssxp 6067 ofrfvalg 7705 ofval 7708 ofrval 7709 off 7715 ofres 7716 ofco 7722 dftpos4 8270 smores2 8394 dmttrcl 9761 rnttrcl 9762 onwf 9870 r0weon 10052 dju1dif 10213 unctb 10244 infmap2 10257 itunitc 10461 axcclem 10497 dfnn3 12280 cotr2 15016 ressbasssg 17282 ressbasssOLD 17285 prdsle 17507 prdsless 17508 cntrss 19349 dprd2da 20062 opsrle 22065 indiscld 23099 leordtval2 23220 fiuncmp 23412 prdstopn 23636 ustneism 24232 icchmeo 24971 itg1addlem4 25734 itg1addlem5 25735 aannenlem3 26372 efifo 26589 konigsbergssiedgw 30269 pjoml4i 31606 5oai 31680 3oai 31687 bdopssadj 32100 xrge00 33017 xrge0mulc1cn 33940 esumdivc 34084 rpsqrtcn 34608 subfacp1lem5 35189 filnetlem3 36381 filnetlem4 36382 mblfinlem4 37667 itg2gt0cn 37682 psubspset 39746 psubclsetN 39938 dvrelog2 42065 dvrelog3 42066 readvrec2 42391 relexpaddss 43731 corcltrcl 43752 relopabVD 44921 cncfiooicc 45909 amgmwlem 49321 |
| Copyright terms: Public domain | W3C validator |