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 2977 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1906 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
3 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
4 | 2, 3 | nfan 1891 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓) |
5 | eleq1 2900 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
6 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
7 | 5, 6 | anbi12d 630 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
8 | 1, 4, 7 | spcegf 3591 | . . 3 ⊢ (𝐴 ∈ 𝐵 → ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))) |
9 | 8 | anabsi5 665 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)) |
10 | df-rex 3144 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)) | |
11 | 9, 10 | sylibr 235 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 ∃wex 1771 Ⅎwnf 1775 ∈ wcel 2105 ∃wrex 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rex 3144 df-v 3497 |
This theorem is referenced by: rspcevOLD 3623 reuop 6138 ac6c4 9892 infcvgaux1i 15202 iunmbl2 24087 esumcvg 31245 ptrecube 34774 poimirlem24 34798 sdclem1 34901 uzwo4 41195 eliuniincex 41256 elrnmpt1sf 41330 iuneqfzuzlem 41482 uzublem 41584 uzub 41585 limsuppnfdlem 41862 limsupubuzlem 41873 sge0gerp 42558 smflim 42934 reupr 43531 |
Copyright terms: Public domain | W3C validator |