resabs1d - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > resabs1d		Structured version Visualization version GIF version

Theorem resabs1d 6016

Description: Absorption law for restriction, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypothesis**
Ref	Expression
resabs1d.b	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

**Assertion**
Ref	Expression
resabs1d	⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

**Proof of Theorem resabs1d**
Step	Hyp	Ref	Expression
1		resabs1d.b	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		resabs1 6015	. 2 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1534 ⊆ wss 3947 ↾ cres 5680

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pr 5429

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-opab 5211 df-xp 5684 df-rel 5685 df-res 5690

This theorem is referenced by: f2ndf 8125 frrlem12 8302 ablfac1eulem 20028 funcrngcsetc 20572 funcrngcsetcALT 20573 funcringcsetc 20606 kgencn2 23460 tsmsres 24047 resubmet 24717 xrge0gsumle 24748 cmssmscld 25277 cmsss 25278 cmscsscms 25300 minveclem3a 25354 dvmptresicc 25844 dvlip2 25927 c1liplem1 25928 efcvx 26385 logccv 26596 loglesqrt 26692 wilthlem2 27000 nosupno 27635 nosupbnd1lem1 27640 nosupbnd2 27648 noinfno 27650 noinfbnd1lem1 27655 noinfbnd2 27663 symgcom2 32807 cyc3conja 32878 bnj1280 34651 cvmlift2lem9 34921 mbfresfi 37139 ssbnd 37261 prdsbnd2 37268 cnpwstotbnd 37270 reheibor 37312 diophin 42192 fnwe2lem2 42475 dvsid 43768 limcresiooub 45030 limcresioolb 45031 fourierdlem46 45540 fourierdlem48 45542 fourierdlem49 45543 fourierdlem58 45552 fourierdlem72 45566 fourierdlem73 45567 fourierdlem74 45568 fourierdlem75 45569 fourierdlem89 45583 fourierdlem90 45584 fourierdlem91 45585 fourierdlem93 45587 fourierdlem100 45594 fourierdlem102 45596 fourierdlem103 45597 fourierdlem104 45598 fourierdlem107 45601 fourierdlem111 45605 fourierdlem112 45606 fourierdlem114 45608 afvres 46552 afv2res 46619

	
		OSZAR »