![]() |
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 5100 |
. 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 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-nfc 2581 df-v 3047 df-in 3411 df-opab 4462 df-xp 4840 df-res 4846 |
This theorem is referenced by: reseq12i 5103 rescom 5129 rescnvcnv 5298 resdm2 5325 funcnvres 5652 resasplit 5753 fresaunres2 5755 fresaunres1 5756 resdif 5834 resin 5835 fvn0ssdmfun 6013 residpr 6068 wfrlem5 7040 domss2 7731 ordtypelem1 8033 ackbij2lem3 8671 facnn 12461 fac0 12462 hashresfn 12523 relexpcnv 13098 divcnvshft 13913 ruclem4 14286 fsets 15149 setsid 15164 meet0 16383 join0 16384 symgfixelsi 17076 psgnsn 17161 dprd2da 17675 ply1plusgfvi 18835 uptx 20640 txcn 20641 ressxms 21540 ressms 21541 iscmet3lem3 22260 volres 22482 dvlip 22945 dvne0 22963 lhop 22968 dflog2 23510 dfrelog 23515 dvlog 23596 wilthlem2 23994 0pth 25300 2pthlem1 25325 ghsubgolemOLD 26098 zrdivrng 26160 df1stres 28284 df2ndres 28285 ffsrn 28314 resf1o 28315 fpwrelmapffs 28319 sitmcl 29184 eulerpartlemn 29214 bnj1326 29835 divcnvlin 30367 frrlem5 30518 poimirlem9 31949 isdrngo1 32195 eldioph4b 35654 diophren 35656 rclexi 36222 rtrclex 36224 cnvrcl0 36232 dfrtrcl5 36236 dfrcl2 36266 relexpiidm 36296 relexp01min 36305 relexpaddss 36310 seff 36657 sblpnf 36658 radcnvrat 36663 hashnzfzclim 36671 dvresioo 37793 fourierdlem72 38042 fourierdlem80 38050 fourierdlem94 38064 fourierdlem103 38073 fourierdlem104 38074 fourierdlem113 38083 fouriersw 38095 sge0split 38251 0grsubgr 39350 rngcidALTV 40046 ringcidALTV 40109 |
Copyright terms: Public domain | W3C validator |