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

Theorem rspcedv 3308
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 238 . 2 ((𝜑𝑥 = 𝐴) → (𝜒𝜓))
41, 3rspcimedv 3306 1 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  wrex 2910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-v 3197
This theorem is referenced by:  rspcebdv  3309  rspcedvd  3312  fsuppmapnn0fiubOLD  12774  wrdl1exs1  13376  0csh0  13520  gcdcllem1  15202  nn0gsumfz  18361  pmatcollpw3lem  20569  pmatcollpw3fi1lem2  20573  pm2mpfo  20600  f1otrg  25732  cusgrfilem2  26333  wwlksnredwwlkn  26771  wwlksnextprop  26788  clwwlksnun  26954  cusconngr  27031  xrofsup  29507  esum2d  30129  rexzrexnn0  37187  ov2ssiunov2  37811  lcoel0  41982  lcoss  41990  el0ldep  42020  ldepspr  42027  islindeps2  42037  isldepslvec2  42039
  Copyright terms: Public domain W3C validator