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

Theorem rspcedv 3574
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 250 . 2 ((𝜑𝑥 = 𝐴) → (𝜒𝜓))
41, 3rspcimedv 3572 1 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 399   = wceq 1560  wcel 2142  wrex 3086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734
This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087
This theorem is referenced by:  rspcebdv  3575  rspcev  3581  rspcedvd  3583  0csh0  14806  gcdcllem1  16533  nn0gsumfz  20024  pmatcollpw3lem  22840  pmatcollpw3fi1lem2  22844  pm2mpfo  22871  f1otrg  29068  cusgrfilem2  29654  wwlksnredwwlkn  30092  wwlksnextprop  30109  clwwlknun  30311  cusconngr  30390  xrofsup  32966  esum2d  34387  rexzrexnn0  43378  onsucelab  43837  ordnexbtwnsuc  43841  ov2ssiunov2  44273  requad2  48242  lcoel0  49047  lcoss  49055  el0ldep  49085  ldepspr  49092  islindeps2  49102  isldepslvec2  49104  affinecomb1  49321  isisod  49645
  Copyright terms: Public domain W3C validator