Theorem rspcedvd 3586

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093

This theorem is used by:  rspcime  3589  fsnex  7292  updjud  9939  modfzo0difsn  13999  ssnn0fi  14041  fsuppmapnn0fiubex  14048  tpfo  14557  wrdl1exs1  14673  swrdrn3  14714  cshimadifsn0  14893  reusq0  15542  divconjdvds  16398  2tp1odd  16435  dfgcd2  16629  fissn0dvds  16702  ncoprmlnprm  16812  dvdsprmpweq  16969  oddprmdvds  16988  prmgaplem2  17135  prmgaplcmlem2  17137  prmgaplem5  17140  prmgapprmolem  17146  fullestrcsetc  18232  equivestrcsetc  18233  fullsetcestrc  18247  isnsgrp  18810  efmndmnd  18979  smndex1mnd  19003  smndex1n0mnd  19005  mgmnsgrpex  19024  sgrpnmndex  19025  dfgrp2  19060  grplrinv  19094  grpidinv  19096  dfgrp3  19136  cycsubmcl  19303  cycsubm  19304  ghmquskerlem1  19384  ringid  20389  ringadd2  20391  ringunitnzdiv  20513  rngisomring  20582  rngqiprngimfo  21478  ring2idlqus  21486  pzriprnglem10  21677  pzriprnglem11  21678  cply1coe0bi  22499  evls1maprnss  22575  scmatid  22708  scmataddcl  22710  scmatsubcl  22711  scmatmulcl  22712  scmatrhmcl  22722  mat0scmat  22732  symgmatr01lem  22847  cpmatacl  22910  cpmatinvcl  22911  m2cpmfo  22950  pmatcollpw3fi1lem2  22981  gausslemma2dlem1a  27566  2lgslem1b  27593  addsq2reu  27641  addsqrexnreu  27643  addsq2nreurex  27645  2sqreulem1  27647  2sqreunnlem1  27650  islnoppd  29058  outpasch  29074  hlpasch  29075  colopp  29088  colhp  29089  isinagd  29193  inaghl  29199  isleagd  29202  f1otrg  29257  usgredg4  29604  nbupgr  29731  nbumgrvtx  29733  nbgr2vtx1edg  29737  nbuhgr2vtx1edgb  29739  nbusgredgeu  29753  cusgrexilem2  29829  wlkvtxiedg  30011  elwwlks2ons3  30341  umgr2cwwkdifex  30453  1pthon2ve  30542  numclwwlk1lem2fo  30746  2ndimaxp  33028  1stpreimas  33088  cshwrnid  33312  gsummpt2d  33400  gsumhashmul  33418  cyc3genpmlem  33502  cyc3genpm  33503  cycpmconjs  33507  cyc3conja  33508  elrgspnlem1  33593  elrgspnsubrunlem2  33599  erlbrd  33614  erler  33616  rloccring  33622  rlocisunit  33627  fldgenval  33664  dvdsruassoi  33728  dvdsruasso  33729  lsmsnidl  33741  grplsmid  33744  quslsm  33745  nsgmgc  33752  nsgqusf1olem1  33753  nsgqusf1olem2  33754  nsgqusf1olem3  33755  elrspunidl  33767  elrspunsn  33768  mxidlprm  33784  qsdrngilem  33807  1arithidom  33858  fedgmul  34052  ccfldextdgrr  34093  fldextrspunlsplem  34094  irngss  34108  irngnzply1lem  34111  constrsslem  34162  constrconj  34166  constrfiss  34172  constrllcllem  34173  constrlccllem  34174  constrcccllem  34175  nn0constr  34182  ist0cld  34254  zarclsun  34291  zarclsint  34293  zarcmplem  34302  rhmpreimacn  34306  esum2d  34514  reprsuc  35034  reprpmtf1o  35045  fmlasuc  35899  fmla1  35900  satffunlem1lem2  35916  satffunlem2lem2  35919  sategoelfvb  35932  2goelgoanfmla1  35937  unblimceq0lem  37136  unblimceq0  37137  unbdqndv2  37141  knoppndvlem19  37160  aks4d1  42897  primrootsunit1  42905  primrootscoprmpow  42907  primrootscoprbij  42910  remexz  42912  aks6d1c2p2  42927  hashscontpow1  42929  aks6d1c6isolem1  42982  aks6d1c6lem5  42985  unitscyglem5  43007  aks5lem8  43009  3rspcedvd  43028  oacl2g  44098  omcl2  44101  ofoaf  44123  dfno2  44195  clsk3nimkb  44807  clsk1indlem1  44812  ntrclsiso  44834  ntrclsk2  44835  ntrclskb  44836  ntrclsk3  44837  ntrclsk13  44838  ntrclsk4  44839  imo72b2lem0  44932  imo72b2lem2  44934  imo72b2lem1  44936  imo72b2  44939  mnuprdlem4  45026  mnuunid  45028  mnurndlem2  45033  restsubel  45912  fsupdm  47597  finfdm  47601  fsetsniunop  47827  fsetsnf  47829  cfsetsnfsetf  47836  cfsetsnfsetfo  47838  2reu8i  47891  mod0mul  48140  nndivides2  48162  preimafvelsetpreimafv  48178  imasetpreimafvbijlemfo  48195  iccelpart  48223  fargshiftfo  48232  sprsymrelf1lem  48281  sprsymrelfo  48287  prproropf1o  48297  paireqne  48301  nprmmul3  48319  fmtnoodd  48326  fmtnoprmfac2lem1  48359  fmtnofac2lem  48361  fmtnofac2  48362  fmtnofac1  48363  41prothprm  48412  requad01  48427  dfodd6  48443  dfeven4  48444  opoeALTV  48489  opeoALTV  48490  nn0onn0exALTV  48505  nn0enn0exALTV  48506  nnennexALTV  48507  mogoldbblem  48526  sbgoldbst  48584  sgoldbeven3prm  48589  sbgoldbo  48593  nnsum3primesgbe  48598  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  evengpop3  48604  evengpoap3  48605  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  wtgoldbnnsum4prm  48608  bgoldbnnsum3prm  48610  bgoldbtbndlem4  48614  bgoldbtbnd  48615  bgoldbachlt  48619  tgoldbachlt  48622  predgclnbgrel  48645  clnbgredg  48646  clnbgrgrimlem  48739  grlimgredgex  48806  gpgprismgriedgdmss  48858  gpgedgvtx0  48867  gpgedgiov  48871  gpg3kgrtriexlem6  48894  gpg3kgrtriex  48895  uspgrsprfo  48954  1odd  48977  nnsgrpnmnd  48984  0even  49043  2even  49045  2zlidl  49046  2zrngamgm  49051  2zrngamnd  49053  2zrngagrp  49055  2zrngmmgm  49058  2zrngnmlid  49061  ply1mulgsumlem1  49207  ply1mulgsumlem2  49208  el0ldep  49287  nn0onn0ex  49344  nn0enn0ex  49345  nnennex  49346  nnpw2p  49407  1arymaptfo  49464  2arymaptfo  49475  eenglngeehlnmlem1  49558  eenglngeehlnmlem2  49559  rrx2vlinest  49562  itsclquadb  49597  iunlub  49640  iinglb  49641