rspc - Metamath Proof Explorer

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

Theorem rspc 3596

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)

**Hypotheses**
Ref	Expression
rspc.1	⊢ Ⅎ𝑥𝜓
rspc.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

**Assertion**
Ref	Expression
rspc	⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 Allowed substitution hints: 𝜑(𝑥) 𝜓(𝑥)

**Proof of Theorem rspc**
Step	Hyp	Ref	Expression
1		df-ral 3052	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2892	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1910	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1892	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2814	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 343	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3577	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 241	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∀wal 1532 = wceq 1534 Ⅎwnf 1778 ∈ wcel 2099 ∀wral 3051

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-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ral 3052 df-v 3464

This theorem is referenced by: rspc2 3617 rspc2vd 3943 disjxiun 5150 pofun 5612 fmptcof 7144 fliftfuns 7326 ofmpteq 7712 tfisg 7864 qliftfuns 8833 xpf1o 9177 iunfi 9385 iundom2g 10583 lble 12218 rlimcld2 15580 sumeq2ii 15697 summolem3 15718 zsum 15722 fsum 15724 fsumf1o 15727 sumss2 15730 fsumcvg2 15731 fsumadd 15744 isummulc2 15766 fsum2dlem 15774 fsumcom2 15778 fsumshftm 15785 fsum0diag2 15787 fsummulc2 15788 fsum00 15802 fsumabs 15805 fsumrelem 15811 fsumrlim 15815 fsumo1 15816 o1fsum 15817 fsumiun 15825 isumshft 15843 prodeq2ii 15915 prodmolem3 15935 zprod 15939 fprod 15943 fprodf1o 15948 prodss 15949 fprodser 15951 fprodmul 15962 fproddiv 15963 fprodm1s 15972 fprodp1s 15973 fprodabs 15976 fprod2dlem 15982 fprodcom2 15986 fprodefsum 16097 sumeven 16389 sumodd 16390 pcmpt 16894 invfuc 17999 dprd2d2 20044 txcnp 23615 ptcnplem 23616 prdsdsf 24364 prdsxmet 24366 fsumcn 24879 ovolfiniun 25521 ovoliunnul 25527 volfiniun 25567 iunmbl 25573 limciun 25914 dvfsumle 26045 dvfsumleOLD 26046 dvfsumabs 26048 dvfsumlem1 26051 dvfsumlem3 26054 dvfsumlem4 26055 dvfsumrlim 26057 dvfsumrlim2 26058 dvfsum2 26060 itgsubst 26075 fsumvma 27242 dchrisumlema 27517 dchrisumlem2 27519 dchrisumlem3 27520 nosupbnd1 27744 noinfbnd1 27759 chirred 32328 fsumiunle 32730 sigapildsyslem 33994 voliune 34062 volfiniune 34063 ptrest 37320 poimirlem25 37346 poimirlem26 37347 mzpsubst 42405 rabdiophlem2 42459 cvgcaule 45107 etransclem48 45903 sge0iunmpt 46039 2reu8i 46726

	
		OSZAR »