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

Theorem rspcedv 3532
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 240 . 2 ((𝜑𝑥 = 𝐴) → (𝜒𝜓))
41, 3rspcimedv 3530 1 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1508  wcel 2051  wrex 3082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2743
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-ral 3086  df-rex 3087  df-v 3410
This theorem is referenced by:  rspcebdv  3533  rspcedvd  3535  0csh0  14014  0csh0OLD  14015  gcdcllem1  15706  nn0gsumfz  18866  pmatcollpw3lem  21110  pmatcollpw3fi1lem2  21114  pm2mpfo  21141  f1otrg  26375  cusgrfilem2  26956  wwlksnredwwlkn  27399  wwlksnredwwlknOLD  27400  wwlksnextprop  27430  wwlksnextpropOLD  27431  clwwlknun  27655  cusconngr  27735  xrofsup  30268  esum2d  31028  rexzrexnn0  38835  ov2ssiunov2  39446  requad2  43190  lcoel0  43884  lcoss  43892  el0ldep  43922  ldepspr  43929  islindeps2  43939  isldepslvec2  43941  affinecomb1  44091
  Copyright terms: Public domain W3C validator