Theorem rspcedvd 3580

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by:  rspcime  3583  rspcedeq1vd  3585  rspcedeq2vd  3586  fsnex  7239  updjud  9858  modfzo0difsn  13878  ssnn0fi  13920  fsuppmapnn0fiubex  13927  tpfo  14435  wrdl1exs1  14549  cshimadifsn0  14765  reusq0  15400  divconjdvds  16254  2tp1odd  16291  dfgcd2  16485  fissn0dvds  16558  ncoprmlnprm  16667  dvdsprmpweq  16824  oddprmdvds  16843  prmgaplem2  16990  prmgaplcmlem2  16992  prmgaplem5  16995  prmgapprmolem  17001  fullestrcsetc  18086  equivestrcsetc  18087  fullsetcestrc  18101  isnsgrp  18660  efmndmnd  18826  smndex1mnd  18847  smndex1n0mnd  18849  mgmnsgrpex  18868  sgrpnmndex  18869  dfgrp2  18904  grplrinv  18938  grpidinv  18940  dfgrp3  18981  cycsubmcl  19142  cycsubm  19143  ghmquskerlem1  19224  ringid  20221  ringadd2  20223  ringunitnzdiv  20346  rngisomring  20415  rngqiprngimfo  21268  ring2idlqus  21276  pzriprnglem10  21457  pzriprnglem11  21458  cply1coe0bi  22258  evls1maprnss  22334  scmatid  22470  scmataddcl  22472  scmatsubcl  22473  scmatmulcl  22474  scmatrhmcl  22484  mat0scmat  22494  symgmatr01lem  22609  cpmatacl  22672  cpmatinvcl  22673  m2cpmfo  22712  pmatcollpw3fi1lem2  22743  gausslemma2dlem1a  27344  2lgslem1b  27371  addsq2reu  27419  addsqrexnreu  27421  addsq2nreurex  27423  2sqreulem1  27425  2sqreunnlem1  27428  islnoppd  28824  outpasch  28839  hlpasch  28840  colopp  28853  colhp  28854  isinagd  28923  inaghl  28929  isleagd  28932  f1otrg  28955  usgredg4  29302  nbupgr  29429  nbumgrvtx  29431  nbgr2vtx1edg  29435  nbuhgr2vtx1edgb  29437  nbusgredgeu  29451  cusgrexilem2  29527  wlkvtxiedg  29710  elwwlks2ons3  30040  umgr2cwwkdifex  30152  1pthon2ve  30241  numclwwlk1lem2fo  30445  2ndimaxp  32735  1stpreimas  32795  swrdrn3  33047  cshwrnid  33053  gsummpt2d  33142  gsumhashmul  33160  cyc3genpmlem  33244  cyc3genpm  33245  cycpmconjs  33249  cyc3conja  33250  elrgspnlem1  33335  elrgspnsubrunlem2  33341  erlbrd  33356  erler  33358  rloccring  33363  fldgenval  33405  dvdsruassoi  33476  dvdsruasso  33477  lsmsnidl  33491  grplsmid  33496  quslsm  33497  nsgmgc  33504  nsgqusf1olem1  33505  nsgqusf1olem2  33506  nsgqusf1olem3  33507  elrspunidl  33520  elrspunsn  33521  mxidlprm  33562  mxidlirredi  33563  qsdrngilem  33586  1arithidom  33629  fedgmul  33808  ccfldextdgrr  33849  fldextrspunlsplem  33850  irngss  33864  irngnzply1lem  33867  constrsslem  33918  constrconj  33922  constrfiss  33928  constrllcllem  33929  constrlccllem  33930  constrcccllem  33931  nn0constr  33938  ist0cld  34010  zarclsun  34047  zarclsint  34049  zarcmplem  34058  rhmpreimacn  34062  esum2d  34270  reprsuc  34792  reprpmtf1o  34803  fmlasuc  35599  fmla1  35600  satffunlem1lem2  35616  satffunlem2lem2  35619  sategoelfvb  35632  2goelgoanfmla1  35637  unblimceq0lem  36725  unblimceq0  36726  unbdqndv2  36730  knoppndvlem19  36749  aks4d1  42453  primrootsunit1  42461  primrootscoprmpow  42463  primrootscoprbij  42466  remexz  42468  aks6d1c2p2  42483  hashscontpow1  42485  aks6d1c6isolem1  42538  aks6d1c6lem5  42541  unitscyglem5  42563  aks5lem8  42565  3rspcedvd  42582  oacl2g  43681  omcl2  43684  ofoaf  43706  dfno2  43778  clsk3nimkb  44390  clsk1indlem1  44395  ntrclsiso  44417  ntrclsk2  44418  ntrclskb  44419  ntrclsk3  44420  ntrclsk13  44421  ntrclsk4  44422  imo72b2lem0  44515  imo72b2lem2  44517  imo72b2lem1  44519  imo72b2  44522  mnuprdlem4  44625  mnuunid  44627  mnurndlem2  44632  restsubel  45506  fsupdm  47194  finfdm  47198  fsetsniunop  47403  fsetsnf  47405  cfsetsnfsetf  47412  cfsetsnfsetfo  47414  2reu8i  47467  mod0mul  47710  preimafvelsetpreimafv  47742  imasetpreimafvbijlemfo  47759  iccelpart  47787  fargshiftfo  47796  sprsymrelf1lem  47845  sprsymrelfo  47851  prproropf1o  47861  paireqne  47865  fmtnoodd  47887  fmtnoprmfac2lem1  47920  fmtnofac2lem  47922  fmtnofac2  47923  fmtnofac1  47924  41prothprm  47973  requad01  47975  dfodd6  47991  dfeven4  47992  opoeALTV  48037  opeoALTV  48038  nn0onn0exALTV  48053  nn0enn0exALTV  48054  nnennexALTV  48055  mogoldbblem  48074  sbgoldbst  48132  sgoldbeven3prm  48137  sbgoldbo  48141  nnsum3primesgbe  48146  nnsum4primesodd  48150  nnsum4primesoddALTV  48151  evengpop3  48152  evengpoap3  48153  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  wtgoldbnnsum4prm  48156  bgoldbnnsum3prm  48158  bgoldbtbndlem4  48162  bgoldbtbnd  48163  bgoldbachlt  48167  tgoldbachlt  48170  predgclnbgrel  48193  clnbgredg  48194  clnbgrgrimlem  48287  grlimgredgex  48354  gpgprismgriedgdmss  48406  gpgedgvtx0  48415  gpgedgiov  48419  gpg3kgrtriexlem6  48442  gpg3kgrtriex  48443  uspgrsprfo  48502  1odd  48525  nnsgrpnmnd  48532  0even  48591  2even  48593  2zlidl  48594  2zrngamgm  48599  2zrngamnd  48601  2zrngagrp  48603  2zrngmmgm  48606  2zrngnmlid  48609  ply1mulgsumlem1  48740  ply1mulgsumlem2  48741  el0ldep  48820  nn0onn0ex  48877  nn0enn0ex  48878  nnennex  48879  nnpw2p  48940  1arymaptfo  48997  2arymaptfo  49008  eenglngeehlnmlem1  49091  eenglngeehlnmlem2  49092  rrx2vlinest  49095  itsclquadb  49130  iunlub  49174  iinglb  49175