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

Theorem rspce 3611
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 2905 . . . 4 𝑥𝐴
2 nfv 1914 . . . . 5 𝑥 𝐴𝐵
3 rspc.1 . . . . 5 𝑥𝜓
42, 3nfan 1899 . . . 4 𝑥(𝐴𝐵𝜓)
5 eleq1 2829 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6anbi12d 632 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
81, 4, 7spcegf 3592 . . 3 (𝐴𝐵 → ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑)))
98anabsi5 669 . 2 ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑))
10 df-rex 3071 . 2 (∃𝑥𝐵 𝜑 ↔ ∃𝑥(𝑥𝐵𝜑))
119, 10sylibr 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