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

Theorem rspcedv 3286
 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 237 . 2 ((𝜑𝑥 = 𝐴) → (𝜒𝜓))
41, 3rspcimedv 3284 1 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ 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-ral 2901  df-rex 2902  df-v 3175 This theorem is referenced by:  rspcedvd  3289  fsuppmapnn0fiubOLD  12653  wrdl1exs1  13246  0csh0  13390  gcdcllem1  15059  nn0gsumfz  18203  pmatcollpw3lem  20407  pmatcollpw3fi1lem2  20411  pm2mpfo  20438  f1otrg  25551  cusgrafilem2  26008  wwlknredwwlkn  26254  wwlkextprop  26272  xrofsup  28923  esum2d  29482  rexzrexnn0  36386  ov2ssiunov2  37011  cusgrfilem2  40672  wwlksnredwwlkn  41101  wwlksnextprop  41118  clwwlksnun  41281  cusconngr  41358  lcoel0  42011  lcoss  42019  el0ldep  42049  ldepspr  42056  islindeps2  42066  isldepslvec2  42068
 Copyright terms: Public domain W3C validator