Theorem rspcedvd 3566

Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 3557. (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 3557	. 2 ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
5	1, 4	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3061

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062

This theorem is referenced by:  rspcime  3569  fsnex  7238  updjud  9858  modfzo0difsn  13905  ssnn0fi  13947  fsuppmapnn0fiubex  13954  tpfo  14462  wrdl1exs1  14576  cshimadifsn0  14792  reusq0  15427  divconjdvds  16284  2tp1odd  16321  dfgcd2  16515  fissn0dvds  16588  ncoprmlnprm  16698  dvdsprmpweq  16855  oddprmdvds  16874  prmgaplem2  17021  prmgaplcmlem2  17023  prmgaplem5  17026  prmgapprmolem  17032  fullestrcsetc  18117  equivestrcsetc  18118  fullsetcestrc  18132  isnsgrp  18691  efmndmnd  18857  smndex1mnd  18881  smndex1n0mnd  18883  mgmnsgrpex  18902  sgrpnmndex  18903  dfgrp2  18938  grplrinv  18972  grpidinv  18974  dfgrp3  19015  cycsubmcl  19176  cycsubm  19177  ghmquskerlem1  19258  ringid  20255  ringadd2  20257  ringunitnzdiv  20378  rngisomring  20447  rngqiprngimfo  21299  ring2idlqus  21307  pzriprnglem10  21470  pzriprnglem11  21471  cply1coe0bi  22267  evls1maprnss  22343  scmatid  22479  scmataddcl  22481  scmatsubcl  22482  scmatmulcl  22483  scmatrhmcl  22493  mat0scmat  22503  symgmatr01lem  22618  cpmatacl  22681  cpmatinvcl  22682  m2cpmfo  22721  pmatcollpw3fi1lem2  22752  gausslemma2dlem1a  27328  2lgslem1b  27355  addsq2reu  27403  addsqrexnreu  27405  addsq2nreurex  27407  2sqreulem1  27409  2sqreunnlem1  27412  islnoppd  28808  outpasch  28823  hlpasch  28824  colopp  28837  colhp  28838  isinagd  28907  inaghl  28913  isleagd  28916  f1otrg  28939  usgredg4  29286  nbupgr  29413  nbumgrvtx  29415  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  nbusgredgeu  29435  cusgrexilem2  29511  wlkvtxiedg  29693  elwwlks2ons3  30023  umgr2cwwkdifex  30135  1pthon2ve  30224  numclwwlk1lem2fo  30428  2ndimaxp  32719  1stpreimas  32779  swrdrn3  33015  cshwrnid  33021  gsummpt2d  33110  gsumhashmul  33128  cyc3genpmlem  33212  cyc3genpm  33213  cycpmconjs  33217  cyc3conja  33218  elrgspnlem1  33303  elrgspnsubrunlem2  33309  erlbrd  33324  erler  33326  rloccring  33331  fldgenval  33373  dvdsruassoi  33444  dvdsruasso  33445  lsmsnidl  33459  grplsmid  33464  quslsm  33465  nsgmgc  33472  nsgqusf1olem1  33473  nsgqusf1olem2  33474  nsgqusf1olem3  33475  elrspunidl  33488  elrspunsn  33489  mxidlprm  33530  mxidlirredi  33531  qsdrngilem  33554  1arithidom  33597  fedgmul  33775  ccfldextdgrr  33816  fldextrspunlsplem  33817  irngss  33831  irngnzply1lem  33834  constrsslem  33885  constrconj  33889  constrfiss  33895  constrllcllem  33896  constrlccllem  33897  constrcccllem  33898  nn0constr  33905  ist0cld  33977  zarclsun  34014  zarclsint  34016  zarcmplem  34025  rhmpreimacn  34029  esum2d  34237  reprsuc  34759  reprpmtf1o  34770  fmlasuc  35568  fmla1  35569  satffunlem1lem2  35585  satffunlem2lem2  35588  sategoelfvb  35601  2goelgoanfmla1  35606  unblimceq0lem  36766  unblimceq0  36767  unbdqndv2  36771  knoppndvlem19  36790  aks4d1  42528  primrootsunit1  42536  primrootscoprmpow  42538  primrootscoprbij  42541  remexz  42543  aks6d1c2p2  42558  hashscontpow1  42560  aks6d1c6isolem1  42613  aks6d1c6lem5  42616  unitscyglem5  42638  aks5lem8  42640  3rspcedvd  42657  oacl2g  43758  omcl2  43761  ofoaf  43783  dfno2  43855  clsk3nimkb  44467  clsk1indlem1  44472  ntrclsiso  44494  ntrclsk2  44495  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  ntrclsk4  44499  imo72b2lem0  44592  imo72b2lem2  44594  imo72b2lem1  44596  imo72b2  44599  mnuprdlem4  44702  mnuunid  44704  mnurndlem2  44709  restsubel  45583  fsupdm  47270  finfdm  47274  fsetsniunop  47497  fsetsnf  47499  cfsetsnfsetf  47506  cfsetsnfsetfo  47508  2reu8i  47561  mod0mul  47810  nndivides2  47832  preimafvelsetpreimafv  47848  imasetpreimafvbijlemfo  47865  iccelpart  47893  fargshiftfo  47902  sprsymrelf1lem  47951  sprsymrelfo  47957  prproropf1o  47967  paireqne  47971  nprmmul3  47989  fmtnoodd  47996  fmtnoprmfac2lem1  48029  fmtnofac2lem  48031  fmtnofac2  48032  fmtnofac1  48033  41prothprm  48082  requad01  48097  dfodd6  48113  dfeven4  48114  opoeALTV  48159  opeoALTV  48160  nn0onn0exALTV  48175  nn0enn0exALTV  48176  nnennexALTV  48177  mogoldbblem  48196  sbgoldbst  48254  sgoldbeven3prm  48259  sbgoldbo  48263  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  evengpop3  48274  evengpoap3  48275  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem4  48284  bgoldbtbnd  48285  bgoldbachlt  48289  tgoldbachlt  48292  predgclnbgrel  48315  clnbgredg  48316  clnbgrgrimlem  48409  grlimgredgex  48476  gpgprismgriedgdmss  48528  gpgedgvtx0  48537  gpgedgiov  48541  gpg3kgrtriexlem6  48564  gpg3kgrtriex  48565  uspgrsprfo  48624  1odd  48647  nnsgrpnmnd  48654  0even  48713  2even  48715  2zlidl  48716  2zrngamgm  48721  2zrngamnd  48723  2zrngagrp  48725  2zrngmmgm  48728  2zrngnmlid  48731  ply1mulgsumlem1  48862  ply1mulgsumlem2  48863  el0ldep  48942  nn0onn0ex  48999  nn0enn0ex  49000  nnennex  49001  nnpw2p  49062  1arymaptfo  49119  2arymaptfo  49130  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2vlinest  49217  itsclquadb  49252  iunlub  49296  iinglb  49297