Theorem rspcedvd 3578

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061

This theorem is referenced by:  rspcime  3581  rspcedeq1vd  3583  rspcedeq2vd  3584  fsnex  7229  updjud  9846  modfzo0difsn  13866  ssnn0fi  13908  fsuppmapnn0fiubex  13915  tpfo  14423  wrdl1exs1  14537  cshimadifsn0  14753  reusq0  15388  divconjdvds  16242  2tp1odd  16279  dfgcd2  16473  fissn0dvds  16546  ncoprmlnprm  16655  dvdsprmpweq  16812  oddprmdvds  16831  prmgaplem2  16978  prmgaplcmlem2  16980  prmgaplem5  16983  prmgapprmolem  16989  fullestrcsetc  18074  equivestrcsetc  18075  fullsetcestrc  18089  isnsgrp  18648  efmndmnd  18814  smndex1mnd  18835  smndex1n0mnd  18837  mgmnsgrpex  18856  sgrpnmndex  18857  dfgrp2  18892  grplrinv  18926  grpidinv  18928  dfgrp3  18969  cycsubmcl  19130  cycsubm  19131  ghmquskerlem1  19212  ringid  20209  ringadd2  20211  ringunitnzdiv  20334  rngisomring  20403  rngqiprngimfo  21256  ring2idlqus  21264  pzriprnglem10  21445  pzriprnglem11  21446  cply1coe0bi  22246  evls1maprnss  22322  scmatid  22458  scmataddcl  22460  scmatsubcl  22461  scmatmulcl  22462  scmatrhmcl  22472  mat0scmat  22482  symgmatr01lem  22597  cpmatacl  22660  cpmatinvcl  22661  m2cpmfo  22700  pmatcollpw3fi1lem2  22731  gausslemma2dlem1a  27332  2lgslem1b  27359  addsq2reu  27407  addsqrexnreu  27409  addsq2nreurex  27411  2sqreulem1  27413  2sqreunnlem1  27416  islnoppd  28812  outpasch  28827  hlpasch  28828  colopp  28841  colhp  28842  isinagd  28911  inaghl  28917  isleagd  28920  f1otrg  28943  usgredg4  29290  nbupgr  29417  nbumgrvtx  29419  nbgr2vtx1edg  29423  nbuhgr2vtx1edgb  29425  nbusgredgeu  29439  cusgrexilem2  29515  wlkvtxiedg  29698  elwwlks2ons3  30028  umgr2cwwkdifex  30140  1pthon2ve  30229  numclwwlk1lem2fo  30433  2ndimaxp  32724  1stpreimas  32785  swrdrn3  33037  cshwrnid  33043  gsummpt2d  33132  gsumhashmul  33150  cyc3genpmlem  33233  cyc3genpm  33234  cycpmconjs  33238  cyc3conja  33239  elrgspnlem1  33324  elrgspnsubrunlem2  33330  erlbrd  33345  erler  33347  rloccring  33352  fldgenval  33394  dvdsruassoi  33465  dvdsruasso  33466  lsmsnidl  33480  grplsmid  33485  quslsm  33486  nsgmgc  33493  nsgqusf1olem1  33494  nsgqusf1olem2  33495  nsgqusf1olem3  33496  elrspunidl  33509  elrspunsn  33510  mxidlprm  33551  mxidlirredi  33552  qsdrngilem  33575  1arithidom  33618  fedgmul  33788  ccfldextdgrr  33829  fldextrspunlsplem  33830  irngss  33844  irngnzply1lem  33847  constrsslem  33898  constrconj  33902  constrfiss  33908  constrllcllem  33909  constrlccllem  33910  constrcccllem  33911  nn0constr  33918  ist0cld  33990  zarclsun  34027  zarclsint  34029  zarcmplem  34038  rhmpreimacn  34042  esum2d  34250  reprsuc  34772  reprpmtf1o  34783  fmlasuc  35580  fmla1  35581  satffunlem1lem2  35597  satffunlem2lem2  35600  sategoelfvb  35613  2goelgoanfmla1  35618  unblimceq0lem  36706  unblimceq0  36707  unbdqndv2  36711  knoppndvlem19  36730  aks4d1  42339  primrootsunit1  42347  primrootscoprmpow  42349  primrootscoprbij  42352  remexz  42354  aks6d1c2p2  42369  hashscontpow1  42371  aks6d1c6isolem1  42424  aks6d1c6lem5  42427  unitscyglem5  42449  aks5lem8  42451  3rspcedvd  42468  oacl2g  43568  omcl2  43571  ofoaf  43593  dfno2  43665  clsk3nimkb  44277  clsk1indlem1  44282  ntrclsiso  44304  ntrclsk2  44305  ntrclskb  44306  ntrclsk3  44307  ntrclsk13  44308  ntrclsk4  44309  imo72b2lem0  44402  imo72b2lem2  44404  imo72b2lem1  44406  imo72b2  44409  mnuprdlem4  44512  mnuunid  44514  mnurndlem2  44519  restsubel  45393  fsupdm  47082  finfdm  47086  fsetsniunop  47291  fsetsnf  47293  cfsetsnfsetf  47300  cfsetsnfsetfo  47302  2reu8i  47355  mod0mul  47598  preimafvelsetpreimafv  47630  imasetpreimafvbijlemfo  47647  iccelpart  47675  fargshiftfo  47684  sprsymrelf1lem  47733  sprsymrelfo  47739  prproropf1o  47749  paireqne  47753  fmtnoodd  47775  fmtnoprmfac2lem1  47808  fmtnofac2lem  47810  fmtnofac2  47811  fmtnofac1  47812  41prothprm  47861  requad01  47863  dfodd6  47879  dfeven4  47880  opoeALTV  47925  opeoALTV  47926  nn0onn0exALTV  47941  nn0enn0exALTV  47942  nnennexALTV  47943  mogoldbblem  47962  sbgoldbst  48020  sgoldbeven3prm  48025  sbgoldbo  48029  nnsum3primesgbe  48034  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  evengpop3  48040  evengpoap3  48041  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  wtgoldbnnsum4prm  48044  bgoldbnnsum3prm  48046  bgoldbtbndlem4  48050  bgoldbtbnd  48051  bgoldbachlt  48055  tgoldbachlt  48058  predgclnbgrel  48081  clnbgredg  48082  clnbgrgrimlem  48175  grlimgredgex  48242  gpgprismgriedgdmss  48294  gpgedgvtx0  48303  gpgedgiov  48307  gpg3kgrtriexlem6  48330  gpg3kgrtriex  48331  uspgrsprfo  48390  1odd  48413  nnsgrpnmnd  48420  0even  48479  2even  48481  2zlidl  48482  2zrngamgm  48487  2zrngamnd  48489  2zrngagrp  48491  2zrngmmgm  48494  2zrngnmlid  48497  ply1mulgsumlem1  48628  ply1mulgsumlem2  48629  el0ldep  48708  nn0onn0ex  48765  nn0enn0ex  48766  nnennex  48767  nnpw2p  48828  1arymaptfo  48885  2arymaptfo  48896  eenglngeehlnmlem1  48979  eenglngeehlnmlem2  48980  rrx2vlinest  48983  itsclquadb  49018  iunlub  49062  iinglb  49063