![]() |
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 2460 |
. 2
![]() ![]() ![]() ![]() |
3 | eqsstr3.2 |
. 2
![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqsstri 3462 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-in 3411 df-ss 3418 |
This theorem is referenced by: inss2 3653 dmv 5050 ofrfval 6539 ofval 6540 ofrval 6541 off 6546 ofres 6547 ofco 6551 dftpos4 6992 smores2 7073 onwf 8301 r0weon 8443 cda1dif 8606 unctb 8635 infmap2 8648 itunitc 8851 axcclem 8887 dfnn3 10623 bcm1k 12500 bcpasc 12506 cotr2 13041 ressbasss 15181 strlemor1 15217 prdsle 15360 prdsless 15361 dprd2da 17675 opsrle 18699 indiscld 20107 leordtval2 20228 fiuncmp 20419 prdstopn 20643 ustneism 21238 itg1addlem4 22657 itg1addlem5 22658 tdeglem4 23009 aannenlem3 23286 efifo 23496 advlogexp 23600 pjoml4i 27240 5oai 27314 3oai 27321 bdopssadj 27734 suppss2fOLD 28237 xrge00 28448 xrge0mulc1cn 28747 esumdivc 28904 ballotlemodife 29330 subfacp1lem5 29907 filnetlem3 31036 filnetlem4 31037 mblfinlem4 31980 itg2gt0cn 31997 psubspset 33309 psubclsetN 33501 relexpaddss 36310 corcltrcl 36331 relopabVD 37298 cncfiooicc 37772 stoweidlem34 37895 |
Copyright terms: Public domain | W3C validator |