Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reseq2 | Structured version Visualization version GIF version |
Description: Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.) |
Ref | Expression |
---|---|
reseq2 | ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1 5572 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V)) | |
2 | 1 | ineq2d 4192 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V))) |
3 | df-res 5570 | . 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V)) | |
4 | df-res 5570 | . 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V)) | |
5 | 2, 3, 4 | 3eqtr4g 2884 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 Vcvv 3497 ∩ cin 3938 × cxp 5556 ↾ cres 5560 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-rab 3150 df-in 3946 df-opab 5132 df-xp 5564 df-res 5570 |
This theorem is referenced by: reseq2i 5853 reseq2d 5856 resabs1 5886 resima2 5891 imaeq2 5928 resdisj 6029 fimadmfoALT 6604 fressnfv 6925 tfrlem1 8015 tfrlem9 8024 tfrlem11 8027 tfrlem12 8028 tfr2b 8035 tz7.44-1 8045 tz7.44-2 8046 tz7.44-3 8047 rdglem1 8054 fnfi 8799 fseqenlem1 9453 rtrclreclem4 14423 psgnprfval1 18653 gsumzaddlem 19044 gsum2dlem2 19094 znunithash 20714 islinds 20956 lmbr2 21870 lmff 21912 kgencn2 22168 ptcmpfi 22424 tsmsgsum 22750 tsmsres 22755 tsmsf1o 22756 tsmsxplem1 22764 tsmsxp 22766 ustval 22814 xrge0gsumle 23444 xrge0tsms 23445 lmmbr2 23865 lmcau 23919 limcun 24496 jensen 25569 wilthlem2 25649 wilthlem3 25650 hhssnvt 29045 hhsssh 29049 foresf1o 30268 reldisjun 30356 xrge0tsmsd 30696 gsumle 30729 esumsnf 31327 subfacp1lem3 32433 subfacp1lem5 32435 erdszelem1 32442 erdsze 32453 erdsze2lem2 32455 cvmscbv 32509 cvmshmeo 32522 cvmsss2 32525 dfpo2 32995 eldm3 33001 dfrdg2 33044 bj-diagval 34470 mbfresfi 34942 elcoeleqvrels 35834 eleldisjs 35965 eldisjeq 35978 mzpcompact2lem 39354 seff 40647 wessf1ornlem 41451 fouriersw 42523 sge0tsms 42669 sge0f1o 42671 sge0sup 42680 meadjuni 42746 ismeannd 42756 psmeasurelem 42759 psmeasure 42760 omeunile 42794 isomennd 42820 hoidmvlelem3 42886 |
Copyright terms: Public domain | W3C validator |