Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspce Structured version   Visualization version   GIF version

Theorem rspce 3444
 Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.)
Hypotheses
Ref Expression
rspc.1 𝑥𝜓
rspc.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspce ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rspce
StepHypRef Expression
1 nfcv 2902 . . . 4 𝑥𝐴
2 nfv 1992 . . . . 5 𝑥 𝐴𝐵
3 rspc.1 . . . . 5 𝑥𝜓
42, 3nfan 1977 . . . 4 𝑥(𝐴𝐵𝜓)
5 eleq1 2827 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6anbi12d 749 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
81, 4, 7spcegf 3429 . . 3 (𝐴𝐵 → ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑)))
98anabsi5 893 . 2 ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑))
10 df-rex 3056 . 2 (∃𝑥𝐵 𝜑 ↔ ∃𝑥(𝑥𝐵𝜑))
119, 10sylibr 224 1 ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632  ∃wex 1853  Ⅎwnf 1857   ∈ wcel 2139  ∃wrex 3051 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-v 3342 This theorem is referenced by:  rspcev  3449  ac6c4  9495  fsumcom2OLD  14705  infcvgaux1i  14788  fprodcom2OLD  14914  iunmbl2  23525  esumcvg  30457  ptrecube  33722  poimirlem24  33746  sdclem1  33852  uzwo4  39720  eliuniincex  39791  wessf1ornlem  39870  elrnmpt1sf  39875  iuneqfzuzlem  40048  uzublem  40155  uzub  40156  limsuppnfdlem  40436  limsupubuzlem  40447  sge0gerp  41115  smflim  41491
 Copyright terms: Public domain W3C validator