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

Theorem rspce 3277
 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 2751 . . . 4 𝑥𝐴
2 nfv 1830 . . . . 5 𝑥 𝐴𝐵
3 rspc.1 . . . . 5 𝑥𝜓
42, 3nfan 1816 . . . 4 𝑥(𝐴𝐵𝜓)
5 eleq1 2676 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6anbi12d 743 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
81, 4, 7spcegf 3262 . . 3 (𝐴𝐵 → ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑)))
98anabsi5 854 . 2 ((𝐴𝐵𝜓) → ∃𝑥(𝑥𝐵𝜑))
10 df-rex 2902 . 2 (∃𝑥𝐵 𝜑 ↔ ∃𝑥(𝑥𝐵𝜑))
119, 10sylibr 223 1 ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175 This theorem is referenced by:  rspcev  3282  ac6c4  9186  fsumcom2OLD  14348  infcvgaux1i  14428  fprodcom2OLD  14554  iunmbl2  23132  esumcvg  29475  ptrecube  32579  poimirlem24  32603  sdclem1  32709  uzwo4  38246  eliuniincex  38323  wessf1ornlem  38366  elrnmpt1sf  38371  iuneqfzuzlem  38491  sge0gerp  39288  smflim  39663
 Copyright terms: Public domain W3C validator