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 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090

This theorem is referenced by:  rspcime  3589  fsnex  7271  updjud  9908  modfzo0difsn  13970  ssnn0fi  14012  fsuppmapnn0fiubex  14019  tpfo  14527  wrdl1exs1  14641  cshimadifsn0  14857  reusq0  15506  divconjdvds  16363  2tp1odd  16400  dfgcd2  16594  fissn0dvds  16667  ncoprmlnprm  16777  dvdsprmpweq  16934  oddprmdvds  16953  prmgaplem2  17100  prmgaplcmlem2  17102  prmgaplem5  17105  prmgapprmolem  17111  fullestrcsetc  18197  equivestrcsetc  18198  fullsetcestrc  18212  isnsgrp  18771  efmndmnd  18938  smndex1mnd  18962  smndex1n0mnd  18964  mgmnsgrpex  18983  sgrpnmndex  18984  dfgrp2  19019  grplrinv  19053  grpidinv  19055  dfgrp3  19096  cycsubmcl  19263  cycsubm  19264  ghmquskerlem1  19344  ringid  20348  ringadd2  20350  ringunitnzdiv  20471  rngisomring  20540  rngqiprngimfo  21403  ring2idlqus  21411  pzriprnglem10  21600  pzriprnglem11  21601  cply1coe0bi  22423  evls1maprnss  22499  scmatid  22632  scmataddcl  22634  scmatsubcl  22635  scmatmulcl  22636  scmatrhmcl  22646  mat0scmat  22656  symgmatr01lem  22771  cpmatacl  22834  cpmatinvcl  22835  m2cpmfo  22874  pmatcollpw3fi1lem2  22905  gausslemma2dlem1a  27487  2lgslem1b  27514  addsq2reu  27562  addsqrexnreu  27564  addsq2nreurex  27566  2sqreulem1  27568  2sqreunnlem1  27571  islnoppd  28971  outpasch  28986  hlpasch  28987  colopp  29000  colhp  29001  isinagd  29091  inaghl  29097  isleagd  29100  f1otrg  29129  usgredg4  29476  nbupgr  29603  nbumgrvtx  29605  nbgr2vtx1edg  29609  nbuhgr2vtx1edgb  29611  nbusgredgeu  29625  cusgrexilem2  29701  wlkvtxiedg  29883  elwwlks2ons3  30213  umgr2cwwkdifex  30325  1pthon2ve  30414  numclwwlk1lem2fo  30618  2ndimaxp  32903  1stpreimas  32963  swrdrn3  33188  cshwrnid  33194  gsummpt2d  33282  gsumhashmul  33300  cyc3genpmlem  33384  cyc3genpm  33385  cycpmconjs  33389  cyc3conja  33390  elrgspnlem1  33475  elrgspnsubrunlem2  33481  erlbrd  33496  erler  33498  rloccring  33504  rlocisunit  33509  fldgenval  33548  dvdsruassoi  33613  dvdsruasso  33614  lsmsnidl  33626  grplsmid  33629  quslsm  33630  nsgmgc  33637  nsgqusf1olem1  33638  nsgqusf1olem2  33639  nsgqusf1olem3  33640  elrspunidl  33652  elrspunsn  33653  mxidlprm  33670  qsdrngilem  33693  1arithidom  33744  fedgmul  33938  ccfldextdgrr  33979  fldextrspunlsplem  33980  irngss  33994  irngnzply1lem  33997  constrsslem  34048  constrconj  34052  constrfiss  34058  constrllcllem  34059  constrlccllem  34060  constrcccllem  34061  nn0constr  34068  ist0cld  34140  zarclsun  34177  zarclsint  34179  zarcmplem  34188  rhmpreimacn  34192  esum2d  34400  reprsuc  34919  reprpmtf1o  34930  fmlasuc  35749  fmla1  35750  satffunlem1lem2  35766  satffunlem2lem2  35769  sategoelfvb  35782  2goelgoanfmla1  35787  unblimceq0lem  36957  unblimceq0  36958  unbdqndv2  36962  knoppndvlem19  36981  aks4d1  42718  primrootsunit1  42726  primrootscoprmpow  42728  primrootscoprbij  42731  remexz  42733  aks6d1c2p2  42748  hashscontpow1  42750  aks6d1c6isolem1  42803  aks6d1c6lem5  42806  unitscyglem5  42828  aks5lem8  42830  3rspcedvd  42847  oacl2g  43919  omcl2  43922  ofoaf  43944  dfno2  44016  clsk3nimkb  44628  clsk1indlem1  44633  ntrclsiso  44655  ntrclsk2  44656  ntrclskb  44657  ntrclsk3  44658  ntrclsk13  44659  ntrclsk4  44660  imo72b2lem0  44753  imo72b2lem2  44755  imo72b2lem1  44757  imo72b2  44760  mnuprdlem4  44849  mnuunid  44851  mnurndlem2  44856  restsubel  45729  fsupdm  47414  finfdm  47418  fsetsniunop  47641  fsetsnf  47643  cfsetsnfsetf  47650  cfsetsnfsetfo  47652  2reu8i  47705  mod0mul  47954  nndivides2  47976  preimafvelsetpreimafv  47992  imasetpreimafvbijlemfo  48009  iccelpart  48037  fargshiftfo  48046  sprsymrelf1lem  48095  sprsymrelfo  48101  prproropf1o  48111  paireqne  48115  nprmmul3  48133  fmtnoodd  48140  fmtnoprmfac2lem1  48173  fmtnofac2lem  48175  fmtnofac2  48176  fmtnofac1  48177  41prothprm  48226  requad01  48241  dfodd6  48257  dfeven4  48258  opoeALTV  48303  opeoALTV  48304  nn0onn0exALTV  48319  nn0enn0exALTV  48320  nnennexALTV  48321  mogoldbblem  48340  sbgoldbst  48398  sgoldbeven3prm  48403  sbgoldbo  48407  nnsum3primesgbe  48412  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  evengpop3  48418  evengpoap3  48419  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  wtgoldbnnsum4prm  48422  bgoldbnnsum3prm  48424  bgoldbtbndlem4  48428  bgoldbtbnd  48429  bgoldbachlt  48433  tgoldbachlt  48436  predgclnbgrel  48459  clnbgredg  48460  clnbgrgrimlem  48553  grlimgredgex  48620  gpgprismgriedgdmss  48672  gpgedgvtx0  48681  gpgedgiov  48685  gpg3kgrtriexlem6  48708  gpg3kgrtriex  48709  uspgrsprfo  48768  1odd  48791  nnsgrpnmnd  48798  0even  48857  2even  48859  2zlidl  48860  2zrngamgm  48865  2zrngamnd  48867  2zrngagrp  48869  2zrngmmgm  48872  2zrngnmlid  48875  ply1mulgsumlem1  49017  ply1mulgsumlem2  49018  el0ldep  49097  nn0onn0ex  49154  nn0enn0ex  49155  nnennex  49156  nnpw2p  49217  1arymaptfo  49274  2arymaptfo  49285  eenglngeehlnmlem1  49368  eenglngeehlnmlem2  49369  rrx2vlinest  49372  itsclquadb  49407  iunlub  49450  iinglb  49451