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 3063 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
2 | nfcv 2905 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfv 1915 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
4 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1897 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
6 | eleq1 2824 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
7 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
8 | 6, 7 | imbi12d 345 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
9 | 2, 5, 8 | spcgf 3535 | . . 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 1537 = wceq 1539 Ⅎwnf 1783 ∈ wcel 2104 ∀wral 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-tru 1542 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ral 3063 df-v 3439 |
This theorem is referenced by: rspc2 3573 rspc2vd 3888 disjxiun 5078 pofun 5532 fmptcof 7034 fliftfuns 7217 ofmpteq 7587 qliftfuns 8624 xpf1o 8964 iunfi 9155 iundom2g 10346 lble 11977 rlimcld2 15336 sumeq2ii 15454 summolem3 15475 zsum 15479 fsum 15481 fsumf1o 15484 sumss2 15487 fsumcvg2 15488 fsumadd 15501 isummulc2 15523 fsum2dlem 15531 fsumcom2 15535 fsumshftm 15542 fsum0diag2 15544 fsummulc2 15545 fsum00 15559 fsumabs 15562 fsumrelem 15568 fsumrlim 15572 fsumo1 15573 o1fsum 15574 fsumiun 15582 isumshft 15600 prodeq2ii 15672 prodmolem3 15692 zprod 15696 fprod 15700 fprodf1o 15705 prodss 15706 fprodser 15708 fprodmul 15719 fproddiv 15720 fprodm1s 15729 fprodp1s 15730 fprodabs 15733 fprod2dlem 15739 fprodcom2 15743 fprodefsum 15853 sumeven 16145 sumodd 16146 pcmpt 16642 invfuc 17741 dprd2d2 19696 txcnp 22820 ptcnplem 22821 prdsdsf 23569 prdsxmet 23571 fsumcn 24082 ovolfiniun 24714 ovoliunnul 24720 volfiniun 24760 iunmbl 24766 limciun 25107 dvfsumle 25234 dvfsumabs 25236 dvfsumlem1 25239 dvfsumlem3 25241 dvfsumlem4 25242 dvfsumrlim 25244 dvfsumrlim2 25245 dvfsum2 25247 itgsubst 25262 fsumvma 26410 dchrisumlema 26685 dchrisumlem2 26687 dchrisumlem3 26688 chirred 30806 fsumiunle 31192 sigapildsyslem 32178 voliune 32246 volfiniune 32247 tfisg 33835 nosupbnd1 33966 noinfbnd1 33981 ptrest 35824 poimirlem25 35850 poimirlem26 35851 mzpsubst 40765 rabdiophlem2 40819 etransclem48 44052 sge0iunmpt 44186 2reu8i 44849 |
Copyright terms: Public domain | W3C validator |