| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rspce | Structured version Visualization version GIF version | ||
| Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.) |
| Ref | Expression |
|---|---|
| rspc.1 | ⊢ Ⅎ𝑥𝜓 |
| rspc.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| rspce | ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfcv 2905 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
| 2 | nfv 1914 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
| 3 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
| 4 | 2, 3 | nfan 1899 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓) |
| 5 | eleq1 2829 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
| 6 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 7 | 5, 6 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
| 8 | 1, 4, 7 | spcegf 3592 | . . 3 ⊢ (𝐴 ∈ 𝐵 → ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))) |
| 9 | 8 | anabsi5 669 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)) |
| 10 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)) | |
| 11 | 9, 10 | sylibr 234 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 Ⅎwnf 1783 ∈ wcel 2108 ∃wrex 3070 |
| 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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-cleq 2729 df-clel 2816 df-nfc 2892 df-rex 3071 |
| This theorem is referenced by: reuop 6313 ac6c4 10521 infcvgaux1i 15893 iunmbl2 25592 gsumpart 33060 esumcvg 34087 ptrecube 37627 poimirlem24 37651 sdclem1 37750 uzwo4 45058 eliuniincex 45114 elrnmpt1sf 45194 iuneqfzuzlem 45345 uzublem 45441 uzub 45442 limsupubuzlem 45727 sge0gerp 46410 smflim 46792 reupr 47509 |
| Copyright terms: Public domain | W3C validator |