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

Theorem rspcedv 3576
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 3574 1 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wb 209  wa 401   = wceq 1570  wcel 2146  wrex 3091
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737
This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092
This theorem is used by:  rspcebdv  3577  rspcev  3583  rspcedvd  3585  0csh0  14854  gcdcllem1  16579  nn0gsumfz  20098  pmatcollpw3lem  22990  pmatcollpw3fi1lem2  22994  pm2mpfo  23021  f1otrg  29275  cusgrfilem2  29864  wwlksnredwwlkn  30311  wwlksnextprop  30328  clwwlknun  30530  cusconngr  30613  xrofsup  33182  esum2d  34547  rexzrexnn0  43589  onsucelab  44048  ordnexbtwnsuc  44052  ov2ssiunov2  44484  requad2  48446  lcoel0  49265  lcoss  49273  el0ldep  49303  ldepspr  49310  islindeps2  49320  isldepslvec2  49322  affinecomb1  49539  isisod  49862
  Copyright terms: Public domain W3C validator