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 2977 . . . 4 𝑥𝐴
2 nfv 1906 . . . . 5 𝑥 𝐴𝐵
3 rspc.1 . . . . 5 𝑥𝜓
42, 3nfan 1891 . . . 4 𝑥(𝐴𝐵𝜓)
5 eleq1 2900 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6anbi12d 630 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
81, 4, 7spcegf 3591 . . 3 (𝐴𝐵 → ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑)))
98anabsi5 665 . 2 ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑))
10 df-rex 3144 . 2 (∃𝑥𝐵 𝜑 ↔ ∃𝑥(𝑥𝐵𝜑))
119, 10sylibr 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