![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reseq2i | Structured version Visualization version Unicode version |
Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
reseqi.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
reseq2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseqi.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | reseq2 5106 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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-nfc 2601 df-v 3033 df-in 3397 df-opab 4455 df-xp 4845 df-res 4851 |
This theorem is referenced by: reseq12i 5109 rescom 5135 rescnvcnv 5305 resdm2 5332 funcnvres 5662 resasplit 5765 fresaunres2 5767 fresaunres1 5768 resdif 5848 resin 5849 fvn0ssdmfun 6028 residpr 6084 wfrlem5 7058 domss2 7749 ordtypelem1 8051 ackbij2lem3 8689 facnn 12499 fac0 12500 hashresfn 12561 relexpcnv 13175 divcnvshft 13990 ruclem4 14363 fsets 15227 setsid 15242 meet0 16461 join0 16462 symgfixelsi 17154 psgnsn 17239 dprd2da 17753 ply1plusgfvi 18912 uptx 20717 txcn 20718 ressxms 21618 ressms 21619 iscmet3lem3 22338 volres 22560 dvlip 23024 dvne0 23042 lhop 23047 dflog2 23589 dfrelog 23594 dvlog 23675 wilthlem2 24073 0pth 25379 2pthlem1 25404 ghsubgolemOLD 26179 zrdivrng 26241 df1stres 28359 df2ndres 28360 ffsrn 28389 resf1o 28390 fpwrelmapffs 28394 sitmcl 29257 eulerpartlemn 29287 bnj1326 29907 divcnvlin 30438 frrlem5 30589 poimirlem9 32013 isdrngo1 32259 eldioph4b 35725 diophren 35727 rclexi 36293 rtrclex 36295 cnvrcl0 36303 dfrtrcl5 36307 dfrcl2 36337 relexpiidm 36367 relexp01min 36376 relexpaddss 36381 seff 36727 sblpnf 36728 radcnvrat 36733 hashnzfzclim 36741 dvresioo 37890 fourierdlem72 38154 fourierdlem80 38162 fourierdlem94 38176 fourierdlem103 38185 fourierdlem104 38186 fourierdlem113 38195 fouriersw 38207 sge0split 38365 0grsubgr 39514 0pth-av 40014 1pthdlem1 40023 eupth2lemb 40149 rngcidALTV 40501 ringcidALTV 40564 |
Copyright terms: Public domain | W3C validator |