![]() |
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 3061 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
2 | nfcv 2902 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfv 1917 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
4 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1899 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
6 | eleq1 2820 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
7 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
8 | 6, 7 | imbi12d 344 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
9 | 2, 5, 8 | spcgf 3578 | . . 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 1539 = wceq 1541 Ⅎwnf 1785 ∈ wcel 2106 ∀wral 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-v 3475 |
This theorem is referenced by: rspc2 3616 rspc2vd 3940 disjxiun 5138 pofun 5599 fmptcof 7112 fliftfuns 7295 ofmpteq 7675 tfisg 7826 qliftfuns 8781 xpf1o 9122 iunfi 9323 iundom2g 10517 lble 12148 rlimcld2 15504 sumeq2ii 15621 summolem3 15642 zsum 15646 fsum 15648 fsumf1o 15651 sumss2 15654 fsumcvg2 15655 fsumadd 15668 isummulc2 15690 fsum2dlem 15698 fsumcom2 15702 fsumshftm 15709 fsum0diag2 15711 fsummulc2 15712 fsum00 15726 fsumabs 15729 fsumrelem 15735 fsumrlim 15739 fsumo1 15740 o1fsum 15741 fsumiun 15749 isumshft 15767 prodeq2ii 15839 prodmolem3 15859 zprod 15863 fprod 15867 fprodf1o 15872 prodss 15873 fprodser 15875 fprodmul 15886 fproddiv 15887 fprodm1s 15896 fprodp1s 15897 fprodabs 15900 fprod2dlem 15906 fprodcom2 15910 fprodefsum 16020 sumeven 16312 sumodd 16313 pcmpt 16807 invfuc 17909 dprd2d2 19873 txcnp 23053 ptcnplem 23054 prdsdsf 23802 prdsxmet 23804 fsumcn 24315 ovolfiniun 24947 ovoliunnul 24953 volfiniun 24993 iunmbl 24999 limciun 25340 dvfsumle 25467 dvfsumabs 25469 dvfsumlem1 25472 dvfsumlem3 25474 dvfsumlem4 25475 dvfsumrlim 25477 dvfsumrlim2 25478 dvfsum2 25480 itgsubst 25495 fsumvma 26643 dchrisumlema 26918 dchrisumlem2 26920 dchrisumlem3 26921 nosupbnd1 27144 noinfbnd1 27159 chirred 31511 fsumiunle 31906 sigapildsyslem 32990 voliune 33058 volfiniune 33059 ptrest 36291 poimirlem25 36317 poimirlem26 36318 mzpsubst 41257 rabdiophlem2 41311 cvgcaule 43975 etransclem48 44771 sge0iunmpt 44907 2reu8i 45593 |
Copyright terms: Public domain | W3C validator |