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

Theorem rspce 3615
 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 2981 . . . 4 𝑥𝐴
2 nfv 1908 . . . . 5 𝑥 𝐴𝐵
3 rspc.1 . . . . 5 𝑥𝜓
42, 3nfan 1893 . . . 4 𝑥(𝐴𝐵𝜓)
5 eleq1 2904 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6anbi12d 630 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
81, 4, 7spcegf 3595 . . 3 (𝐴𝐵 → ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑)))
98anabsi5 665 . 2 ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑))
10 df-rex 3148 . 2 (∃𝑥𝐵 𝜑 ↔ ∃𝑥(𝑥𝐵𝜑))
119, 10sylibr 235 1 ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1530  ∃wex 1773  Ⅎwnf 1777   ∈ wcel 2107  ∃wrex 3143 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rex 3148  df-v 3501 This theorem is referenced by:  rspcevOLD  3627  reuop  6141  ac6c4  9895  infcvgaux1i  15204  iunmbl2  24075  esumcvg  31233  ptrecube  34761  poimirlem24  34785  sdclem1  34888  uzwo4  41182  eliuniincex  41243  elrnmpt1sf  41317  iuneqfzuzlem  41469  uzublem  41571  uzub  41572  limsuppnfdlem  41849  limsupubuzlem  41860  sge0gerp  42545  smflim  42921  reupr  43518
 Copyright terms: Public domain W3C validator