![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqsstr3i | Structured version Visualization version Unicode 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 2480 |
. 2
![]() ![]() ![]() ![]() |
3 | eqsstr3.2 |
. 2
![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqsstri 3448 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-in 3397 df-ss 3404 |
This theorem is referenced by: inss2 3644 dmv 5056 ofrfval 6558 ofval 6559 ofrval 6560 off 6565 ofres 6566 ofco 6570 dftpos4 7010 smores2 7091 onwf 8319 r0weon 8461 cda1dif 8624 unctb 8653 infmap2 8666 itunitc 8869 axcclem 8905 dfnn3 10645 bcm1k 12538 bcpasc 12544 cotr2 13116 ressbasss 15259 strlemor1 15295 prdsle 15438 prdsless 15439 dprd2da 17753 opsrle 18776 indiscld 20184 leordtval2 20305 fiuncmp 20496 prdstopn 20720 ustneism 21316 itg1addlem4 22736 itg1addlem5 22737 tdeglem4 23088 aannenlem3 23365 efifo 23575 advlogexp 23679 pjoml4i 27321 5oai 27395 3oai 27402 bdopssadj 27815 suppss2fOLD 28313 xrge00 28523 xrge0mulc1cn 28821 esumdivc 28978 ballotlemodife 29403 subfacp1lem5 29979 filnetlem3 31107 filnetlem4 31108 mblfinlem4 32044 itg2gt0cn 32061 psubspset 33380 psubclsetN 33572 relexpaddss 36381 corcltrcl 36402 relopabVD 37361 cncfiooicc 37869 stoweidlem34 38007 konigsbergssiedgw 40163 |
Copyright terms: Public domain | W3C validator |