![]() |
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 2955 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1915 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | |
3 | rspc.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
4 | 2, 3 | nfan 1900 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓) |
5 | eleq1 2877 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
6 | rspc.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
7 | 5, 6 | anbi12d 633 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
8 | 1, 4, 7 | spcegf 3539 | . . 3 ⊢ (𝐴 ∈ 𝐵 → ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))) |
9 | 8 | anabsi5 668 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)) |
10 | df-rex 3112 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)) | |
11 | 9, 10 | sylibr 237 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∃wex 1781 Ⅎwnf 1785 ∈ wcel 2111 ∃wrex 3107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-rex 3112 df-v 3443 |
This theorem is referenced by: rspcevOLD 3572 reuop 6112 ac6c4 9892 infcvgaux1i 15204 iunmbl2 24161 gsumpart 30740 esumcvg 31455 ptrecube 35057 poimirlem24 35081 sdclem1 35181 uzwo4 41687 eliuniincex 41745 elrnmpt1sf 41816 iuneqfzuzlem 41966 uzublem 42067 uzub 42068 limsupubuzlem 42354 sge0gerp 43034 smflim 43410 reupr 44039 |
Copyright terms: Public domain | W3C validator |