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 2901 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
2 | nfcv 2751 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfv 1830 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
4 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1813 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
6 | eleq1 2676 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
7 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
8 | 6, 7 | imbi12d 333 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
9 | 2, 5, 8 | spcgf 3261 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓))) |
10 | 9 | pm2.43a 52 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓)) |
11 | 1, 10 | syl5bi 231 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 = wceq 1475 Ⅎwnf 1699 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-v 3175 |
This theorem is referenced by: rspcv 3278 rspc2 3292 disjxiun 4579 disjxiunOLD 4580 pofun 4975 fmptcof 6304 fliftfuns 6464 ofmpteq 6814 qliftfuns 7721 xpf1o 8007 iunfi 8137 iundom2g 9241 lble 10854 rlimcld2 14157 sumeq2ii 14271 summolem3 14292 zsum 14296 fsum 14298 fsumf1o 14301 sumss2 14304 fsumcvg2 14305 fsumadd 14317 isummulc2 14335 fsum2dlem 14343 fsumcom2 14347 fsumcom2OLD 14348 fsumshftm 14355 fsum0diag2 14357 fsummulc2 14358 fsum00 14371 fsumabs 14374 fsumrelem 14380 fsumrlim 14384 fsumo1 14385 o1fsum 14386 fsumiun 14394 isumshft 14410 prodeq2ii 14482 prodmolem3 14502 zprod 14506 fprod 14510 fprodf1o 14515 prodss 14516 fprodser 14518 fprodmul 14529 fproddiv 14530 fprodm1s 14539 fprodp1s 14540 fprodabs 14543 fprod2dlem 14549 fprodcom2 14553 fprodcom2OLD 14554 fprodefsum 14664 sumeven 14948 sumodd 14949 pcmpt 15434 invfuc 16457 dprd2d2 18266 txcnp 21233 ptcnplem 21234 prdsdsf 21982 prdsxmet 21984 fsumcn 22481 ovolfiniun 23076 ovoliunnul 23082 volfiniun 23122 iunmbl 23128 limciun 23464 dvfsumle 23588 dvfsumabs 23590 dvfsumlem1 23593 dvfsumlem3 23595 dvfsumlem4 23596 dvfsumrlim 23598 dvfsumrlim2 23599 dvfsum2 23601 itgsubst 23616 fsumvma 24738 dchrisumlema 24977 dchrisumlem2 24979 dchrisumlem3 24980 chirred 28638 sigapildsyslem 29551 voliune 29619 volfiniune 29620 tfisg 30960 ptrest 32578 poimirlem25 32604 poimirlem26 32605 mzpsubst 36329 rabdiophlem2 36384 etransclem48 39175 sge0iunmpt 39311 rspc2vd 41437 |
Copyright terms: Public domain | W3C validator |