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 2767 | . 2 ⊢ 𝐴 = 𝐵 |
3 | eqsstr3.2 | . 2 ⊢ 𝐵 ⊆ 𝐶 | |
4 | 2, 3 | eqsstri 3926 | 1 ⊢ 𝐴 ⊆ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 ⊆ wss 3858 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2729 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2736 df-cleq 2750 df-clel 2830 df-v 3411 df-in 3865 df-ss 3875 |
This theorem is referenced by: inss2 4134 dmv 5763 idssxp 5888 ofrfvalg 7412 ofval 7415 ofrval 7416 off 7422 ofres 7423 ofco 7427 dftpos4 7921 smores2 8001 onwf 9292 r0weon 9472 dju1dif 9632 unctb 9665 infmap2 9678 itunitc 9881 axcclem 9917 dfnn3 11688 cotr2 14384 ressbasss 16614 prdsle 16793 prdsless 16794 cntrss 18527 dprd2da 19232 opsrle 20807 indiscld 21791 leordtval2 21912 fiuncmp 22104 prdstopn 22328 ustneism 22924 itg1addlem4 24399 itg1addlem5 24400 tdeglem4OLD 24760 aannenlem3 25025 efifo 25238 konigsbergssiedgw 28134 pjoml4i 29469 5oai 29543 3oai 29550 bdopssadj 29963 xrge00 30821 xrge0mulc1cn 31412 esumdivc 31570 rpsqrtcn 32092 subfacp1lem5 32662 filnetlem3 34118 filnetlem4 34119 mblfinlem4 35377 itg2gt0cn 35392 psubspset 37320 psubclsetN 37512 dvrelog2 39630 dvrelog3 39631 relexpaddss 40792 corcltrcl 40813 relopabVD 41980 cncfiooicc 42902 amgmwlem 45721 |
Copyright terms: Public domain | W3C validator |