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 3069 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
2 | nfcv 2907 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfv 1922 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
4 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1904 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
6 | eleq1 2827 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
7 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
8 | 6, 7 | imbi12d 348 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
9 | 2, 5, 8 | spcgf 3521 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓))) |
10 | 9 | pm2.43a 54 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓)) |
11 | 1, 10 | syl5bi 245 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1541 = wceq 1543 Ⅎwnf 1791 ∈ wcel 2112 ∀wral 3064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-nf 1792 df-sb 2073 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ral 3069 df-v 3425 |
This theorem is referenced by: rspcvOLD 3548 rspc2 3560 rspc2vd 3879 disjxiun 5067 pofun 5504 fmptcof 6967 fliftfuns 7145 ofmpteq 7512 qliftfuns 8510 xpf1o 8834 iunfi 8994 iundom2g 10184 lble 11814 rlimcld2 15172 sumeq2ii 15290 summolem3 15311 zsum 15315 fsum 15317 fsumf1o 15320 sumss2 15323 fsumcvg2 15324 fsumadd 15337 isummulc2 15359 fsum2dlem 15367 fsumcom2 15371 fsumshftm 15378 fsum0diag2 15380 fsummulc2 15381 fsum00 15395 fsumabs 15398 fsumrelem 15404 fsumrlim 15408 fsumo1 15409 o1fsum 15410 fsumiun 15418 isumshft 15436 prodeq2ii 15508 prodmolem3 15528 zprod 15532 fprod 15536 fprodf1o 15541 prodss 15542 fprodser 15544 fprodmul 15555 fproddiv 15556 fprodm1s 15565 fprodp1s 15566 fprodabs 15569 fprod2dlem 15575 fprodcom2 15579 fprodefsum 15689 sumeven 15981 sumodd 15982 pcmpt 16478 invfuc 17516 dprd2d2 19464 txcnp 22549 ptcnplem 22550 prdsdsf 23297 prdsxmet 23299 fsumcn 23799 ovolfiniun 24430 ovoliunnul 24436 volfiniun 24476 iunmbl 24482 limciun 24823 dvfsumle 24950 dvfsumabs 24952 dvfsumlem1 24955 dvfsumlem3 24957 dvfsumlem4 24958 dvfsumrlim 24960 dvfsumrlim2 24961 dvfsum2 24963 itgsubst 24978 fsumvma 26126 dchrisumlema 26401 dchrisumlem2 26403 dchrisumlem3 26404 chirred 30508 fsumiunle 30895 sigapildsyslem 31873 voliune 31941 volfiniune 31942 tfisg 33536 nosupbnd1 33688 noinfbnd1 33703 ptrest 35550 poimirlem25 35576 poimirlem26 35577 mzpsubst 40321 rabdiophlem2 40375 etransclem48 43544 sge0iunmpt 43677 2reu8i 44323 |
Copyright terms: Public domain | W3C validator |