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

Theorem rspcedvd 3421
Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 3417. (Contributed by AV, 27-Nov-2019.)
Hypotheses
Ref Expression
rspcedvd.1 (𝜑𝐴𝐵)
rspcedvd.2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
rspcedvd.3 (𝜑𝜒)
Assertion
Ref Expression
rspcedvd (𝜑 → ∃𝑥𝐵 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥   𝜒,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcedvd
StepHypRef Expression
1 rspcedvd.3 . 2 (𝜑𝜒)
2 rspcedvd.1 . . 3 (𝜑𝐴𝐵)
3 rspcedvd.2 . . 3 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
42, 3rspcedv 3417 . 2 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1596  wcel 2103  wrex 3015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-v 3306
This theorem is referenced by:  rspcedeq1vd  3422  rspcedeq2vd  3423  clel5  3448  elpr2elpr  4505  prproe  4542  fsnex  6653  negfi  11084  fiminre  11085  reltre  12284  rpltrp  12285  reltxrnmnf  12286  modmuladd  12827  modmuladdnn0  12829  modfzo0difsn  12857  ssnn0fi  12899  fsuppmapnn0fiubex  12907  cshimadifsn0  13697  divconjdvds  15160  2tp1odd  15199  dfgcd2  15386  fissn0dvds  15455  ncoprmlnprm  15559  dvdsprmpweq  15711  oddprmdvds  15730  prmgaplem2  15877  prmgaplcmlem2  15879  prmgaplem5  15882  prmgapprmolem  15888  fullestrcsetc  16913  equivestrcsetc  16914  fullsetcestrc  16928  isnsgrp  17410  mgmnsgrpex  17540  sgrpnmndex  17541  dfgrp2  17569  grplrinv  17595  grpidinv  17597  dfgrp3  17636  ringid  18695  cply1coe0bi  19793  scmatid  20443  scmataddcl  20445  scmatsubcl  20446  scmatmulcl  20447  scmatrhmcl  20457  mat0scmat  20467  symgmatr01lem  20582  cpmatacl  20644  cpmatinvcl  20645  m2cpmfo  20684  pmatcollpw3fi1lem2  20715  gausslemma2dlem1a  25210  2lgslem1b  25237  islnoppd  25752  outpasch  25767  hlpasch  25768  colopp  25781  colhp  25782  inaghl  25851  f1otrg  25871  usgredg4  26229  nbupgr  26360  nbumgrvtx  26362  nbgr2vtx1edg  26366  nbuhgr2vtx1edgb  26368  nbusgredgeu  26387  cusgrexilem2  26469  wlkvtxiedg  26651  wlkres  26698  elwwlks2ons3  26996  elwwlks2ons3OLD  26997  umgr2cwwkdifex  27117  1pthon2ve  27227  numclwlk1lem2fo  27438  1stpreimas  29713  gsummpt2d  30011  esum2d  30385  reprsuc  30923  reprpmtf1o  30934  unblimceq0lem  32724  unblimceq0  32725  unbdqndv2  32729  knoppndvlem19  32748  clsk3nimkb  38757  clsk1indlem1  38762  ntrclsiso  38784  ntrclsk2  38785  ntrclskb  38786  ntrclsk3  38787  ntrclsk13  38788  ntrclsk4  38789  imo72b2lem0  38884  imo72b2lem2  38886  imo72b2lem1  38890  imo72b2  38894  iccelpart  41796  fargshiftfo  41805  fmtnoodd  41872  fmtnoprmfac2lem1  41905  fmtnofac2lem  41907  fmtnofac2  41908  fmtnofac1  41909  41prothprm  41963  dfodd6  41977  dfeven4  41978  opoeALTV  42021  opeoALTV  42022  nn0onn0exALTV  42036  nn0enn0exALTV  42037  mogoldbblem  42056  sbgoldbst  42093  sgoldbeven3prm  42098  sbgoldbo  42102  nnsum3primesgbe  42107  nnsum4primesodd  42111  nnsum4primesoddALTV  42112  evengpop3  42113  evengpoap3  42114  nnsum4primeseven  42115  nnsum4primesevenALTV  42116  wtgoldbnnsum4prm  42117  bgoldbnnsum3prm  42119  bgoldbtbndlem4  42123  bgoldbtbnd  42124  bgoldbachlt  42128  tgoldbachlt  42131  bgoldbachltOLD  42134  tgoldbachltOLD  42137  sprsymrelf1lem  42168  sprsymrelfo  42174  uspgrsprfo  42183  1odd  42238  nnsgrpnmnd  42245  0even  42358  2even  42360  2zlidl  42361  2zrngamgm  42366  2zrngamnd  42368  2zrngagrp  42370  2zrngmmgm  42373  2zrngnmlid  42376  ply1mulgsumlem1  42601  ply1mulgsumlem2  42602  el0ldep  42682  mod0mul  42741  nn0onn0ex  42745  nn0enn0ex  42746  nnpw2p  42807
  Copyright terms: Public domain W3C validator