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

Theorem rspcedv 3615
Description: Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
rspcdv.1 (𝜑𝐴𝐵)
rspcdv.2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rspcedv (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥   𝜒,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcedv
StepHypRef Expression
1 rspcdv.1 . 2 (𝜑𝐴𝐵)
2 rspcdv.2 . . 3 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
32biimprd 248 . 2 ((𝜑𝑥 = 𝐴) → (𝜒𝜓))
41, 3rspcimedv 3613 1 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  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-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071
This theorem is referenced by:  rspcebdv  3616  rspcev  3622  rspcedvd  3624  0csh0  14831  gcdcllem1  16536  nn0gsumfz  20002  pmatcollpw3lem  22789  pmatcollpw3fi1lem2  22793  pm2mpfo  22820  f1otrg  28879  cusgrfilem2  29474  wwlksnredwwlkn  29915  wwlksnextprop  29932  clwwlknun  30131  cusconngr  30210  xrofsup  32771  esum2d  34094  rexzrexnn0  42815  onsucelab  43276  ordnexbtwnsuc  43280  ov2ssiunov2  43713  requad2  47610  lcoel0  48345  lcoss  48353  el0ldep  48383  ldepspr  48390  islindeps2  48400  isldepslvec2  48402  affinecomb1  48623  isisod  48910
  Copyright terms: Public domain W3C validator