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

Theorem rspcedvd 3625
Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 3615. (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 3615 . 2 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wrex 3139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144
This theorem is referenced by:  rspcime  3626  rspcedeq1vd  3628  rspcedeq2vd  3629  clel5OLD  3657  elpr2elpr  4793  prproe  4830  fsnex  7030  updjud  9352  negfi  11578  fiminreOLD  11579  elpq  12364  reltre  12723  rpltrp  12724  reltxrnmnf  12725  modmuladd  13271  modmuladdnn0  13273  modfzo0difsn  13301  ssnn0fi  13343  fsuppmapnn0fiubex  13350  wrdl1exs1  13957  cshimadifsn0  14182  reusq0  14812  divconjdvds  15655  2tp1odd  15691  dfgcd2  15884  fissn0dvds  15953  ncoprmlnprm  16058  dvdsprmpweq  16210  oddprmdvds  16229  prmgaplem2  16376  prmgaplcmlem2  16378  prmgaplem5  16381  prmgapprmolem  16387  fullestrcsetc  17391  equivestrcsetc  17392  fullsetcestrc  17406  isnsgrp  17895  mgmnsgrpex  18036  sgrpnmndex  18037  dfgrp2  18068  grplrinv  18097  grpidinv  18099  dfgrp3  18138  cycsubmcl  18284  cycsubm  18285  ringid  19255  cply1coe0bi  20398  scmatid  21053  scmataddcl  21055  scmatsubcl  21056  scmatmulcl  21057  scmatrhmcl  21067  mat0scmat  21077  symgmatr01lem  21192  cpmatacl  21254  cpmatinvcl  21255  m2cpmfo  21294  pmatcollpw3fi1lem2  21325  gausslemma2dlem1a  25869  2lgslem1b  25896  addsq2reu  25944  addsqrexnreu  25946  addsq2nreurex  25948  2sqreulem1  25950  2sqreunnlem1  25953  islnoppd  26454  outpasch  26469  hlpasch  26470  colopp  26483  colhp  26484  isinagd  26553  inaghl  26559  isleagd  26562  f1otrg  26585  usgredg4  26927  nbupgr  27054  nbumgrvtx  27056  nbgr2vtx1edg  27060  nbuhgr2vtx1edgb  27062  nbusgredgeu  27076  cusgrexilem2  27152  wlkvtxiedg  27334  elwwlks2ons3  27662  umgr2cwwkdifex  27772  1pthon2ve  27861  numclwwlk1lem2fo  28065  1stpreimas  30368  swrdrn3  30557  cshwrnid  30563  gsummpt2d  30615  cyc3genpmlem  30721  cyc3genpm  30722  cycpmconjs  30726  cyc3conja  30727  fedgmul  30927  ccfldextdgrr  30957  esum2d  31252  reprsuc  31786  reprpmtf1o  31797  fmlasuc  32531  fmla1  32532  satffunlem1lem2  32548  satffunlem2lem2  32551  sategoelfvb  32564  2goelgoanfmla1  32569  unblimceq0lem  33743  unblimceq0  33744  unbdqndv2  33748  knoppndvlem19  33767  3rspcedvd  38985  nnn1suc  39039  prjspertr  39135  prjsperref  39136  prjspersym  39137  prjspvs  39140  0prjspnrel  39149  clsk3nimkb  40270  clsk1indlem1  40275  ntrclsiso  40297  ntrclsk2  40298  ntrclskb  40299  ntrclsk3  40300  ntrclsk13  40301  ntrclsk4  40302  imo72b2lem0  40396  imo72b2lem2  40398  imo72b2lem1  40402  imo72b2  40406  mnuprdlem4  40491  mnuunid  40493  mnurndlem2  40498  2reu8i  43193  iccelpart  43440  fargshiftfo  43449  sprsymrelf1lem  43500  sprsymrelfo  43506  prproropf1o  43516  paireqne  43520  fmtnoodd  43542  fmtnoprmfac2lem1  43575  fmtnofac2lem  43577  fmtnofac2  43578  fmtnofac1  43579  41prothprm  43631  requad01  43633  dfodd6  43649  dfeven4  43650  opoeALTV  43695  opeoALTV  43696  nn0onn0exALTV  43711  nn0enn0exALTV  43712  nnennexALTV  43713  mogoldbblem  43732  sbgoldbst  43790  sgoldbeven3prm  43795  sbgoldbo  43799  nnsum3primesgbe  43804  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  evengpop3  43810  evengpoap3  43811  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  wtgoldbnnsum4prm  43814  bgoldbnnsum3prm  43816  bgoldbtbndlem4  43820  bgoldbtbnd  43821  bgoldbachlt  43825  tgoldbachlt  43828  isomuspgrlem2d  43843  uspgrsprfo  43870  1odd  43925  nnsgrpnmnd  43932  efmndmnd  43956  smndex1mnd  43980  smndex1n0mnd  43982  0even  44100  2even  44102  2zlidl  44103  2zrngamgm  44108  2zrngamnd  44110  2zrngagrp  44112  2zrngmmgm  44115  2zrngnmlid  44118  ply1mulgsumlem1  44338  ply1mulgsumlem2  44339  el0ldep  44419  mod0mul  44477  nn0onn0ex  44481  nn0enn0ex  44482  nnennex  44483  nnpw2p  44544  eenglngeehlnmlem1  44622  eenglngeehlnmlem2  44623  rrx2vlinest  44626  itsclquadb  44661
  Copyright terms: Public domain W3C validator