Theorem rspcedvd 3579

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088

This theorem is used by:  rspcime  3582  fsnex  7283  updjud  9996  modfzo0difsn  14066  ssnn0fi  14108  fsuppmapnn0fiubex  14115  tpfo  14625  wrdl1exs1  14741  swrdrn3  14782  cshimadifsn0  14961  reusq0  15612  divconjdvds  16465  2tp1odd  16502  dfgcd2  16699  fissn0dvds  16774  ncoprmlnprm  16884  dvdsprmpweq  17042  oddprmdvds  17061  prmgaplem2  17208  prmgaplcmlem2  17210  prmgaplem5  17213  prmgapprmolem  17219  fullestrcsetc  18305  equivestrcsetc  18306  fullsetcestrc  18320  isnsgrp  18892  efmndmnd  19065  smndex1mnd  19089  smndex1n0mnd  19091  mgmnsgrpex  19110  sgrpnmndex  19111  dfgrp2  19153  grplrinv  19187  grpidinv  19189  dfgrp3  19229  cycsubmcl  19396  cycsubm  19397  ghmquskerlem1  19477  ringid  20483  ringadd2  20485  ringunitnzdiv  20608  rngisomring  20677  rngqiprngimfo  21577  ring2idlqus  21585  pzriprnglem10  21776  pzriprnglem11  21777  cply1coe0bi  22600  evls1maprnss  22676  scmatid  22809  scmataddcl  22811  scmatsubcl  22812  scmatmulcl  22813  scmatrhmcl  22823  mat0scmat  22833  symgmatr01lem  22948  cpmatacl  23014  cpmatinvcl  23015  m2cpmfo  23054  pmatcollpw3fi1lem2  23085  gausslemma2dlem1a  27674  2lgslem1b  27701  addsq2reu  27749  addsqrexnreu  27751  addsq2nreurex  27753  2sqreulem1  27755  2sqreunnlem1  27758  islnoppd  29198  outpasch  29215  hlpasch  29216  colopp  29229  colhp  29230  isinagd  29340  inaghl  29346  isleagd  29349  f1otrg  29430  usgredg4  29780  nbupgr  29907  nbumgrvtx  29909  nbgr2vtx1edg  29913  nbuhgr2vtx1edgb  29915  nbusgredgeu  29929  cusgrexilem2  30005  wlkvtxiedg  30187  elwwlks2ons3  30526  umgr2cwwkdifex  30638  1pthon2ve  30737  numclwwlk1lem2fo  30941  2ndimaxp  33222  1stpreimas  33281  cshwrnid  33504  gsummpt2d  33592  gsumhashmul  33610  cyc3genpmlem  33694  cyc3genpm  33695  cycpmconjs  33699  cyc3conja  33700  elrgspnlem1  33785  elrgspnsubrunlem2  33791  erlbrd  33806  erler  33808  rloccring  33814  rlocisunit  33819  fldgenval  33856  dvdsruassoi  33921  dvdsruasso  33922  lsmsnidl  33934  grplsmid  33937  quslsm  33938  nsgmgc  33945  nsgqusf1olem1  33946  nsgqusf1olem2  33947  nsgqusf1olem3  33948  elrspunidl  33960  elrspunsn  33961  mxidlprm  33977  qsdrngilem  34000  1arithidom  34051  fedgmul  34245  ccfldextdgrr  34286  fldextrspunlsplem  34287  irngss  34301  irngnzply1lem  34304  constrsslem  34355  constrconj  34359  constrfiss  34365  constrllcllem  34366  constrlccllem  34367  constrcccllem  34368  nn0constr  34375  ist0cld  34447  zarclsun  34484  zarclsint  34486  zarcmplem  34495  rhmpreimacn  34499  esum2d  34707  reprsuc  35227  reprpmtf1o  35238  fmlasuc  36120  fmla1  36121  satffunlem1lem2  36137  satffunlem2lem2  36140  sategoelfvb  36153  2goelgoanfmla1  36158  unblimceq0lem  37342  unblimceq0  37343  unbdqndv2  37347  knoppndvlem19  37366  aks4d1  43107  primrootsunit1  43115  primrootscoprmpow  43117  primrootscoprbij  43120  remexz  43122  aks6d1c2p2  43137  hashscontpow1  43139  aks6d1c6isolem1  43192  aks6d1c6lem5  43195  unitscyglem5  43217  aks5lem8  43219  3rspcedvd  43238  oacl2g  44290  omcl2  44293  ofoaf  44315  dfno2  44387  clsk3nimkb  44999  clsk1indlem1  45004  ntrclsiso  45026  ntrclsk2  45027  ntrclskb  45028  ntrclsk3  45029  ntrclsk13  45030  ntrclsk4  45031  imo72b2lem0  45124  imo72b2lem2  45126  imo72b2lem1  45128  imo72b2  45131  mnuprdlem4  45218  mnuunid  45220  mnurndlem2  45225  restsubel  46111  fsupdm  47796  finfdm  47800  fsetsniunop  48063  fsetsnf  48065  cfsetsnfsetf  48072  cfsetsnfsetfo  48074  2reu8i  48127  mod0mul  48376  nndivides2  48398  preimafvelsetpreimafv  48414  imasetpreimafvbijlemfo  48431  iccelpart  48459  fargshiftfo  48468  sprsymrelf1lem  48517  sprsymrelfo  48523  prproropf1o  48533  paireqne  48537  nprmmul3  48555  fmtnoodd  48562  fmtnoprmfac2lem1  48595  fmtnofac2lem  48597  fmtnofac2  48598  fmtnofac1  48599  41prothprm  48648  requad01  48663  dfodd6  48679  dfeven4  48680  opoeALTV  48725  opeoALTV  48726  nn0onn0exALTV  48741  nn0enn0exALTV  48742  nnennexALTV  48743  mogoldbblem  48762  sbgoldbst  48820  sgoldbeven3prm  48825  sbgoldbo  48829  nnsum3primesgbe  48834  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  evengpop3  48840  evengpoap3  48841  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  wtgoldbnnsum4prm  48844  bgoldbnnsum3prm  48846  bgoldbtbndlem4  48850  bgoldbtbnd  48851  bgoldbachlt  48855  tgoldbachlt  48858  predgclnbgrel  48881  clnbgredg  48882  clnbgrgrimlem  48975  grlimgredgex  49042  gpgprismgriedgdmss  49094  gpgedgvtx0  49103  gpgedgiov  49107  gpg3kgrtriexlem6  49130  gpg3kgrtriex  49131  uspgrsprfo  49190  1odd  49212  nnsgrpnmnd  49219  0even  49278  2even  49280  2zlidl  49281  2zrngamgm  49286  2zrngamnd  49288  2zrngagrp  49290  2zrngmmgm  49293  2zrngnmlid  49296  ply1mulgsumlem1  49442  ply1mulgsumlem2  49443  el0ldep  49522  nn0onn0ex  49579  nn0enn0ex  49580  nnennex  49581  nnpw2p  49642  1arymaptfo  49699  2arymaptfo  49710  eenglngeehlnmlem1  49793  eenglngeehlnmlem2  49794  rrx2vlinest  49797  itsclquadb  49832  iunlub  49875  iinglb  49876