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

Theorem rspcedvd 3623
Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 3613. (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 3613 . 2 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wrex 3136
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 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ral 3140  df-rex 3141
This theorem is referenced by:  rspcime  3624  rspcedeq1vd  3626  rspcedeq2vd  3627  clel5OLD  3655  elpr2elpr  4791  prproe  4828  fsnex  7030  updjud  9351  negfi  11577  fiminreOLD  11578  elpq  12362  reltre  12721  rpltrp  12722  reltxrnmnf  12723  modmuladd  13269  modmuladdnn0  13271  modfzo0difsn  13299  ssnn0fi  13341  fsuppmapnn0fiubex  13348  wrdl1exs1  13955  cshimadifsn0  14180  reusq0  14810  divconjdvds  15653  2tp1odd  15689  dfgcd2  15882  fissn0dvds  15951  ncoprmlnprm  16056  dvdsprmpweq  16208  oddprmdvds  16227  prmgaplem2  16374  prmgaplcmlem2  16376  prmgaplem5  16379  prmgapprmolem  16385  fullestrcsetc  17389  equivestrcsetc  17390  fullsetcestrc  17404  isnsgrp  17893  mgmnsgrpex  18034  sgrpnmndex  18035  dfgrp2  18066  grplrinv  18095  grpidinv  18097  dfgrp3  18136  cycsubmcl  18282  cycsubm  18283  ringid  19253  cply1coe0bi  20396  scmatid  21051  scmataddcl  21053  scmatsubcl  21054  scmatmulcl  21055  scmatrhmcl  21065  mat0scmat  21075  symgmatr01lem  21190  cpmatacl  21252  cpmatinvcl  21253  m2cpmfo  21292  pmatcollpw3fi1lem2  21323  gausslemma2dlem1a  25868  2lgslem1b  25895  addsq2reu  25943  addsqrexnreu  25945  addsq2nreurex  25947  2sqreulem1  25949  2sqreunnlem1  25952  islnoppd  26453  outpasch  26468  hlpasch  26469  colopp  26482  colhp  26483  isinagd  26552  inaghl  26558  isleagd  26561  f1otrg  26584  usgredg4  26926  nbupgr  27053  nbumgrvtx  27055  nbgr2vtx1edg  27059  nbuhgr2vtx1edgb  27061  nbusgredgeu  27075  cusgrexilem2  27151  wlkvtxiedg  27333  elwwlks2ons3  27661  umgr2cwwkdifex  27771  1pthon2ve  27860  numclwwlk1lem2fo  28064  1stpreimas  30367  swrdrn3  30556  cshwrnid  30562  gsummpt2d  30614  cyc3genpmlem  30720  cyc3genpm  30721  cycpmconjs  30725  cyc3conja  30726  fedgmul  30926  ccfldextdgrr  30956  esum2d  31251  reprsuc  31785  reprpmtf1o  31796  fmlasuc  32530  fmla1  32531  satffunlem1lem2  32547  satffunlem2lem2  32550  sategoelfvb  32563  2goelgoanfmla1  32568  unblimceq0lem  33742  unblimceq0  33743  unbdqndv2  33747  knoppndvlem19  33766  3rspcedvd  38983  nnn1suc  39037  prjspertr  39133  prjsperref  39134  prjspersym  39135  prjspvs  39138  0prjspnrel  39147  clsk3nimkb  40268  clsk1indlem1  40273  ntrclsiso  40295  ntrclsk2  40296  ntrclskb  40297  ntrclsk3  40298  ntrclsk13  40299  ntrclsk4  40300  imo72b2lem0  40394  imo72b2lem2  40396  imo72b2lem1  40399  imo72b2  40403  mnuprdlem4  40488  mnuunid  40490  mnurndlem2  40495  2reu8i  43189  preimafvelsetpreimafv  43425  imasetpreimafvbijlemfo  43442  iccelpart  43470  fargshiftfo  43479  sprsymrelf1lem  43530  sprsymrelfo  43536  prproropf1o  43546  paireqne  43550  fmtnoodd  43572  fmtnoprmfac2lem1  43605  fmtnofac2lem  43607  fmtnofac2  43608  fmtnofac1  43609  41prothprm  43661  requad01  43663  dfodd6  43679  dfeven4  43680  opoeALTV  43725  opeoALTV  43726  nn0onn0exALTV  43741  nn0enn0exALTV  43742  nnennexALTV  43743  mogoldbblem  43762  sbgoldbst  43820  sgoldbeven3prm  43825  sbgoldbo  43829  nnsum3primesgbe  43834  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  evengpop3  43840  evengpoap3  43841  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  wtgoldbnnsum4prm  43844  bgoldbnnsum3prm  43846  bgoldbtbndlem4  43850  bgoldbtbnd  43851  bgoldbachlt  43855  tgoldbachlt  43858  isomuspgrlem2d  43873  uspgrsprfo  43900  1odd  43955  nnsgrpnmnd  43962  efmndmnd  43986  smndex1mnd  44010  smndex1n0mnd  44012  0even  44130  2even  44132  2zlidl  44133  2zrngamgm  44138  2zrngamnd  44140  2zrngagrp  44142  2zrngmmgm  44145  2zrngnmlid  44148  ply1mulgsumlem1  44368  ply1mulgsumlem2  44369  el0ldep  44449  mod0mul  44507  nn0onn0ex  44511  nn0enn0ex  44512  nnennex  44513  nnpw2p  44574  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653  rrx2vlinest  44656  itsclquadb  44691
  Copyright terms: Public domain W3C validator