Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rspc | Structured version Visualization version GIF version |
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) |
Ref | Expression |
---|---|
rspc.1 | ⊢ Ⅎ𝑥𝜓 |
rspc.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rspc | ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
2 | nfcv 2977 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfv 1915 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
4 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1897 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
6 | eleq1 2900 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
7 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
8 | 6, 7 | imbi12d 347 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
9 | 2, 5, 8 | spcgf 3590 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓))) |
10 | 9 | pm2.43a 54 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓)) |
11 | 1, 10 | syl5bi 244 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wal 1535 = wceq 1537 Ⅎwnf 1784 ∈ wcel 2114 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-v 3496 |
This theorem is referenced by: rspcvOLD 3619 rspc2 3631 rspc2vd 3932 disjxiun 5063 pofun 5491 fmptcof 6892 fliftfuns 7067 ofmpteq 7428 qliftfuns 8384 xpf1o 8679 iunfi 8812 iundom2g 9962 lble 11593 rlimcld2 14935 sumeq2ii 15050 summolem3 15071 zsum 15075 fsum 15077 fsumf1o 15080 sumss2 15083 fsumcvg2 15084 fsumadd 15096 isummulc2 15117 fsum2dlem 15125 fsumcom2 15129 fsumshftm 15136 fsum0diag2 15138 fsummulc2 15139 fsum00 15153 fsumabs 15156 fsumrelem 15162 fsumrlim 15166 fsumo1 15167 o1fsum 15168 fsumiun 15176 isumshft 15194 prodeq2ii 15267 prodmolem3 15287 zprod 15291 fprod 15295 fprodf1o 15300 prodss 15301 fprodser 15303 fprodmul 15314 fproddiv 15315 fprodm1s 15324 fprodp1s 15325 fprodabs 15328 fprod2dlem 15334 fprodcom2 15338 fprodefsum 15448 sumeven 15738 sumodd 15739 pcmpt 16228 invfuc 17244 dprd2d2 19166 txcnp 22228 ptcnplem 22229 prdsdsf 22977 prdsxmet 22979 fsumcn 23478 ovolfiniun 24102 ovoliunnul 24108 volfiniun 24148 iunmbl 24154 limciun 24492 dvfsumle 24618 dvfsumabs 24620 dvfsumlem1 24623 dvfsumlem3 24625 dvfsumlem4 24626 dvfsumrlim 24628 dvfsumrlim2 24629 dvfsum2 24631 itgsubst 24646 fsumvma 25789 dchrisumlema 26064 dchrisumlem2 26066 dchrisumlem3 26067 chirred 30172 fsumiunle 30545 sigapildsyslem 31420 voliune 31488 volfiniune 31489 tfisg 33055 nosupbnd1 33214 ptrest 34906 poimirlem25 34932 poimirlem26 34933 mzpsubst 39365 rabdiophlem2 39419 etransclem48 42587 sge0iunmpt 42720 2reu8i 43332 |
Copyright terms: Public domain | W3C validator |