Theorem rspcedvd 3569

Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 3560. (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

Step	Hyp	Ref	Expression
1		rspcedvd.3	. 2 ⊢ (𝜑 → 𝜒)
2		rspcedvd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
3		rspcedvd.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
4	2, 3	rspcedv 3560	. 2 ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
5	1, 4	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065

This theorem is referenced by:  rspcime  3572  fsnex  7234  updjud  9856  modfzo0difsn  13903  ssnn0fi  13945  fsuppmapnn0fiubex  13952  tpfo  14460  wrdl1exs1  14574  cshimadifsn0  14790  reusq0  15425  divconjdvds  16282  2tp1odd  16319  dfgcd2  16513  fissn0dvds  16586  ncoprmlnprm  16696  dvdsprmpweq  16853  oddprmdvds  16872  prmgaplem2  17019  prmgaplcmlem2  17021  prmgaplem5  17024  prmgapprmolem  17030  fullestrcsetc  18115  equivestrcsetc  18116  fullsetcestrc  18130  isnsgrp  18689  efmndmnd  18855  smndex1mnd  18879  smndex1n0mnd  18881  mgmnsgrpex  18900  sgrpnmndex  18901  dfgrp2  18936  grplrinv  18970  grpidinv  18972  dfgrp3  19013  cycsubmcl  19174  cycsubm  19175  ghmquskerlem1  19256  ringid  20253  ringadd2  20255  ringunitnzdiv  20376  rngisomring  20445  rngqiprngimfo  21301  ring2idlqus  21309  pzriprnglem10  21472  pzriprnglem11  21473  cply1coe0bi  22295  evls1maprnss  22371  scmatid  22504  scmataddcl  22506  scmatsubcl  22507  scmatmulcl  22508  scmatrhmcl  22518  mat0scmat  22528  symgmatr01lem  22643  cpmatacl  22706  cpmatinvcl  22707  m2cpmfo  22746  pmatcollpw3fi1lem2  22777  gausslemma2dlem1a  27353  2lgslem1b  27380  addsq2reu  27428  addsqrexnreu  27430  addsq2nreurex  27432  2sqreulem1  27434  2sqreunnlem1  27437  islnoppd  28833  outpasch  28848  hlpasch  28849  colopp  28862  colhp  28863  isinagd  28932  inaghl  28938  isleagd  28941  f1otrg  28964  usgredg4  29311  nbupgr  29438  nbumgrvtx  29440  nbgr2vtx1edg  29444  nbuhgr2vtx1edgb  29446  nbusgredgeu  29460  cusgrexilem2  29536  wlkvtxiedg  29718  elwwlks2ons3  30048  umgr2cwwkdifex  30160  1pthon2ve  30249  numclwwlk1lem2fo  30453  2ndimaxp  32745  1stpreimas  32805  swrdrn3  33041  cshwrnid  33047  gsummpt2d  33137  gsumhashmul  33155  cyc3genpmlem  33239  cyc3genpm  33240  cycpmconjs  33244  cyc3conja  33245  elrgspnlem1  33330  elrgspnsubrunlem2  33336  erlbrd  33351  erler  33353  rloccring  33358  fldgenval  33403  dvdsruassoi  33474  dvdsruasso  33475  lsmsnidl  33489  grplsmid  33494  quslsm  33495  nsgmgc  33502  nsgqusf1olem1  33503  nsgqusf1olem2  33504  nsgqusf1olem3  33505  elrspunidl  33518  elrspunsn  33519  mxidlprm  33560  mxidlirredi  33561  qsdrngilem  33584  1arithidom  33627  fedgmul  33822  ccfldextdgrr  33863  fldextrspunlsplem  33864  irngss  33878  irngnzply1lem  33881  constrsslem  33932  constrconj  33936  constrfiss  33942  constrllcllem  33943  constrlccllem  33944  constrcccllem  33945  nn0constr  33952  ist0cld  34024  zarclsun  34061  zarclsint  34063  zarcmplem  34072  rhmpreimacn  34076  esum2d  34284  reprsuc  34806  reprpmtf1o  34817  fmlasuc  35621  fmla1  35622  satffunlem1lem2  35638  satffunlem2lem2  35641  sategoelfvb  35654  2goelgoanfmla1  35659  unblimceq0lem  36819  unblimceq0  36820  unbdqndv2  36824  knoppndvlem19  36843  aks4d1  42581  primrootsunit1  42589  primrootscoprmpow  42591  primrootscoprbij  42594  remexz  42596  aks6d1c2p2  42611  hashscontpow1  42613  aks6d1c6isolem1  42666  aks6d1c6lem5  42669  unitscyglem5  42691  aks5lem8  42693  3rspcedvd  42710  oacl2g  43782  omcl2  43785  ofoaf  43807  dfno2  43879  clsk3nimkb  44491  clsk1indlem1  44496  ntrclsiso  44518  ntrclsk2  44519  ntrclskb  44520  ntrclsk3  44521  ntrclsk13  44522  ntrclsk4  44523  imo72b2lem0  44616  imo72b2lem2  44618  imo72b2lem1  44620  imo72b2  44623  mnuprdlem4  44726  mnuunid  44728  mnurndlem2  44733  restsubel  45607  fsupdm  47292  finfdm  47296  fsetsniunop  47519  fsetsnf  47521  cfsetsnfsetf  47528  cfsetsnfsetfo  47530  2reu8i  47583  mod0mul  47832  nndivides2  47854  preimafvelsetpreimafv  47870  imasetpreimafvbijlemfo  47887  iccelpart  47915  fargshiftfo  47924  sprsymrelf1lem  47973  sprsymrelfo  47979  prproropf1o  47989  paireqne  47993  nprmmul3  48011  fmtnoodd  48018  fmtnoprmfac2lem1  48051  fmtnofac2lem  48053  fmtnofac2  48054  fmtnofac1  48055  41prothprm  48104  requad01  48119  dfodd6  48135  dfeven4  48136  opoeALTV  48181  opeoALTV  48182  nn0onn0exALTV  48197  nn0enn0exALTV  48198  nnennexALTV  48199  mogoldbblem  48218  sbgoldbst  48276  sgoldbeven3prm  48281  sbgoldbo  48285  nnsum3primesgbe  48290  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  evengpop3  48296  evengpoap3  48297  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  wtgoldbnnsum4prm  48300  bgoldbnnsum3prm  48302  bgoldbtbndlem4  48306  bgoldbtbnd  48307  bgoldbachlt  48311  tgoldbachlt  48314  predgclnbgrel  48337  clnbgredg  48338  clnbgrgrimlem  48431  grlimgredgex  48498  gpgprismgriedgdmss  48550  gpgedgvtx0  48559  gpgedgiov  48563  gpg3kgrtriexlem6  48586  gpg3kgrtriex  48587  uspgrsprfo  48646  1odd  48669  nnsgrpnmnd  48676  0even  48735  2even  48737  2zlidl  48738  2zrngamgm  48743  2zrngamnd  48745  2zrngagrp  48747  2zrngmmgm  48750  2zrngnmlid  48753  ply1mulgsumlem1  48884  ply1mulgsumlem2  48885  el0ldep  48964  nn0onn0ex  49021  nn0enn0ex  49022  nnennex  49023  nnpw2p  49084  1arymaptfo  49141  2arymaptfo  49152  eenglngeehlnmlem1  49235  eenglngeehlnmlem2  49236  rrx2vlinest  49239  itsclquadb  49274  iunlub  49318  iinglb  49319