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

Theorem rspcedvd 3348
Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 3344. (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 3344 . 2 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-v 3233
This theorem is referenced by:  rspcedeq1vd  3349  rspcedeq2vd  3350  clel5  3375  elpr2elpr  4429  prproe  4466  fsnex  6578  negfi  11009  fiminre  11010  reltre  12208  rpltrp  12209  reltxrnmnf  12210  modmuladd  12752  modmuladdnn0  12754  modfzo0difsn  12782  ssnn0fi  12824  fsuppmapnn0fiubex  12832  cshimadifsn0  13622  divconjdvds  15084  2tp1odd  15123  dfgcd2  15310  fissn0dvds  15379  ncoprmlnprm  15483  dvdsprmpweq  15635  oddprmdvds  15654  prmgaplem2  15801  prmgaplcmlem2  15803  prmgaplem5  15806  prmgapprmolem  15812  fullestrcsetc  16838  equivestrcsetc  16839  fullsetcestrc  16853  isnsgrp  17335  mgmnsgrpex  17465  sgrpnmndex  17466  dfgrp2  17494  grplrinv  17520  grpidinv  17522  dfgrp3  17561  ringid  18620  cply1coe0bi  19718  scmatid  20368  scmataddcl  20370  scmatsubcl  20371  scmatmulcl  20372  scmatrhmcl  20382  mat0scmat  20392  symgmatr01lem  20507  cpmatacl  20569  cpmatinvcl  20570  m2cpmfo  20609  pmatcollpw3fi1lem2  20640  gausslemma2dlem1a  25135  2lgslem1b  25162  islnoppd  25677  outpasch  25692  hlpasch  25693  colopp  25706  colhp  25707  inaghl  25776  f1otrg  25796  usgredg4  26154  nbupgr  26285  nbumgrvtx  26287  nbgr2vtx1edg  26291  nbuhgr2vtx1edgb  26293  nbusgredgeu  26312  cusgrexilem2  26394  wlkvtxiedg  26576  wlkres  26623  elwwlks2ons3  26920  elwwlks2ons3OLD  26921  umgr2cwwkdifex  27029  1pthon2ve  27132  numclwlk1lem2fo  27348  1stpreimas  29611  gsummpt2d  29909  esum2d  30283  reprsuc  30821  reprpmtf1o  30832  unblimceq0lem  32622  unblimceq0  32623  unbdqndv2  32627  knoppndvlem19  32646  clsk3nimkb  38655  clsk1indlem1  38660  ntrclsiso  38682  ntrclsk2  38683  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  ntrclsk4  38687  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  iccelpart  41694  fargshiftfo  41703  fmtnoodd  41770  fmtnoprmfac2lem1  41803  fmtnofac2lem  41805  fmtnofac2  41806  fmtnofac1  41807  41prothprm  41861  dfodd6  41875  dfeven4  41876  opoeALTV  41919  opeoALTV  41920  nn0onn0exALTV  41934  nn0enn0exALTV  41935  mogoldbblem  41954  sbgoldbst  41991  sgoldbeven3prm  41996  sbgoldbo  42000  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  evengpop3  42011  evengpoap3  42012  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  bgoldbtbndlem4  42021  bgoldbtbnd  42022  bgoldbachlt  42026  tgoldbachlt  42029  bgoldbachltOLD  42032  tgoldbachltOLD  42035  sprsymrelf1lem  42066  sprsymrelfo  42072  uspgrsprfo  42081  1odd  42136  nnsgrpnmnd  42143  0even  42256  2even  42258  2zlidl  42259  2zrngamgm  42264  2zrngamnd  42266  2zrngagrp  42268  2zrngmmgm  42271  2zrngnmlid  42274  ply1mulgsumlem1  42499  ply1mulgsumlem2  42500  el0ldep  42580  mod0mul  42639  nn0onn0ex  42643  nn0enn0ex  42644  nnpw2p  42705
  Copyright terms: Public domain W3C validator