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

Theorem rspcedv 3536
 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 251 . 2 ((𝜑𝑥 = 𝐴) → (𝜒𝜓))
41, 3rspcimedv 3534 1 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃wrex 3071 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076 This theorem is referenced by:  rspcebdv  3537  rspcev  3543  rspcedvd  3546  0csh0  14215  gcdcllem1  15911  nn0gsumfz  19186  pmatcollpw3lem  21497  pmatcollpw3fi1lem2  21501  pm2mpfo  21528  f1otrg  26778  cusgrfilem2  27359  wwlksnredwwlkn  27794  wwlksnextprop  27811  clwwlknun  28010  cusconngr  28089  xrofsup  30627  esum2d  31593  rexzrexnn0  40163  ov2ssiunov2  40819  requad2  44567  lcoel0  45261  lcoss  45269  el0ldep  45299  ldepspr  45306  islindeps2  45316  isldepslvec2  45318  affinecomb1  45540
 Copyright terms: Public domain W3C validator