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

Theorem rspcedvd 3612
Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 3602. (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 3602 . 2 (𝜑 → (𝜒 → ∃𝑥𝐵 𝜓))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wrex 3134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896  df-ral 3138  df-rex 3139
This theorem is referenced by:  rspcime  3613  rspcedeq1vd  3615  rspcedeq2vd  3616  elpr2elpr  4783  prproe  4822  fsnex  7031  updjud  9360  negfi  11586  elpq  12371  reltre  12730  rpltrp  12731  reltxrnmnf  12732  modmuladd  13285  modmuladdnn0  13287  modfzo0difsn  13315  ssnn0fi  13357  fsuppmapnn0fiubex  13364  wrdl1exs1  13967  cshimadifsn0  14192  reusq0  14822  divconjdvds  15665  2tp1odd  15701  dfgcd2  15892  fissn0dvds  15961  ncoprmlnprm  16066  dvdsprmpweq  16218  oddprmdvds  16237  prmgaplem2  16384  prmgaplcmlem2  16386  prmgaplem5  16389  prmgapprmolem  16395  fullestrcsetc  17401  equivestrcsetc  17402  fullsetcestrc  17416  isnsgrp  17905  efmndmnd  18054  smndex1mnd  18075  smndex1n0mnd  18077  mgmnsgrpex  18096  sgrpnmndex  18097  dfgrp2  18128  grplrinv  18157  grpidinv  18159  dfgrp3  18198  cycsubmcl  18344  cycsubm  18345  ringid  19327  cply1coe0bi  20468  scmatid  21123  scmataddcl  21125  scmatsubcl  21126  scmatmulcl  21127  scmatrhmcl  21137  mat0scmat  21147  symgmatr01lem  21262  cpmatacl  21324  cpmatinvcl  21325  m2cpmfo  21364  pmatcollpw3fi1lem2  21395  gausslemma2dlem1a  25952  2lgslem1b  25979  addsq2reu  26027  addsqrexnreu  26029  addsq2nreurex  26031  2sqreulem1  26033  2sqreunnlem1  26036  islnoppd  26537  outpasch  26552  hlpasch  26553  colopp  26566  colhp  26567  isinagd  26636  inaghl  26642  isleagd  26645  f1otrg  26668  usgredg4  27010  nbupgr  27137  nbumgrvtx  27139  nbgr2vtx1edg  27143  nbuhgr2vtx1edgb  27145  nbusgredgeu  27159  cusgrexilem2  27235  wlkvtxiedg  27417  elwwlks2ons3  27744  umgr2cwwkdifex  27853  1pthon2ve  27942  numclwwlk1lem2fo  28146  1stpreimas  30452  swrdrn3  30640  cshwrnid  30646  gsummpt2d  30719  cyc3genpmlem  30825  cyc3genpm  30826  cycpmconjs  30830  cyc3conja  30831  lsmsnidl  30987  mxidlprm  31018  fedgmul  31087  ccfldextdgrr  31117  esum2d  31409  reprsuc  31943  reprpmtf1o  31954  fmlasuc  32690  fmla1  32691  satffunlem1lem2  32707  satffunlem2lem2  32710  sategoelfvb  32723  2goelgoanfmla1  32728  unblimceq0lem  33902  unblimceq0  33903  unbdqndv2  33907  knoppndvlem19  33926  3rspcedvd  39333  nnn1suc  39397  sn-negex12  39483  prjspertr  39515  prjsperref  39516  prjspersym  39517  prjspvs  39520  0prjspnrel  39529  clsk3nimkb  40662  clsk1indlem1  40667  ntrclsiso  40689  ntrclsk2  40690  ntrclskb  40691  ntrclsk3  40692  ntrclsk13  40693  ntrclsk4  40694  imo72b2lem0  40788  imo72b2lem2  40790  imo72b2lem1  40793  imo72b2  40797  mnuprdlem4  40903  mnuunid  40905  mnurndlem2  40910  2reu8i  43595  preimafvelsetpreimafv  43831  imasetpreimafvbijlemfo  43848  iccelpart  43876  fargshiftfo  43885  sprsymrelf1lem  43934  sprsymrelfo  43940  prproropf1o  43950  paireqne  43954  fmtnoodd  43976  fmtnoprmfac2lem1  44009  fmtnofac2lem  44011  fmtnofac2  44012  fmtnofac1  44013  41prothprm  44063  requad01  44065  dfodd6  44081  dfeven4  44082  opoeALTV  44127  opeoALTV  44128  nn0onn0exALTV  44143  nn0enn0exALTV  44144  nnennexALTV  44145  mogoldbblem  44164  sbgoldbst  44222  sgoldbeven3prm  44227  sbgoldbo  44231  nnsum3primesgbe  44236  nnsum4primesodd  44240  nnsum4primesoddALTV  44241  evengpop3  44242  evengpoap3  44243  nnsum4primeseven  44244  nnsum4primesevenALTV  44245  wtgoldbnnsum4prm  44246  bgoldbnnsum3prm  44248  bgoldbtbndlem4  44252  bgoldbtbnd  44253  bgoldbachlt  44257  tgoldbachlt  44260  isomuspgrlem2d  44275  uspgrsprfo  44302  1odd  44357  nnsgrpnmnd  44364  0even  44481  2even  44483  2zlidl  44484  2zrngamgm  44489  2zrngamnd  44491  2zrngagrp  44493  2zrngmmgm  44496  2zrngnmlid  44499  ply1mulgsumlem1  44720  ply1mulgsumlem2  44721  el0ldep  44801  mod0mul  44859  nn0onn0ex  44863  nn0enn0ex  44864  nnennex  44865  nnpw2p  44926  1arymaptfo  44983  2arymaptfo  44994  eenglngeehlnmlem1  45077  eenglngeehlnmlem2  45078  rrx2vlinest  45081  itsclquadb  45116
  Copyright terms: Public domain W3C validator