Theorem rspcedvd 3615

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072

This theorem is referenced by:  rspcime  3617  rspcedeq1vd  3619  rspcedeq2vd  3620  elpr2elpr  4870  prproe  4907  fsnex  7281  fsetfocdm  8855  updjud  9929  negfi  12163  elpq  12959  reltre  13319  rpltrp  13320  reltxrnmnf  13321  modmuladd  13878  modmuladdnn0  13880  modfzo0difsn  13908  ssnn0fi  13950  fsuppmapnn0fiubex  13957  wrdl1exs1  14563  cshimadifsn0  14781  reusq0  15409  divconjdvds  16258  2tp1odd  16295  dfgcd2  16488  fissn0dvds  16556  ncoprmlnprm  16664  dvdsprmpweq  16817  oddprmdvds  16836  prmgaplem2  16983  prmgaplcmlem2  16985  prmgaplem5  16988  prmgapprmolem  16994  fullestrcsetc  18103  equivestrcsetc  18104  fullsetcestrc  18118  isnsgrp  18614  efmndmnd  18770  smndex1mnd  18791  smndex1n0mnd  18793  mgmnsgrpex  18812  sgrpnmndex  18813  dfgrp2  18847  grplrinv  18881  grpidinv  18883  dfgrp3  18922  cycsubmcl  19078  cycsubm  19079  ringid  20091  ringadd2  20093  ringunitnzdiv  20212  cply1coe0bi  21824  scmatid  22016  scmataddcl  22018  scmatsubcl  22019  scmatmulcl  22020  scmatrhmcl  22030  mat0scmat  22040  symgmatr01lem  22155  cpmatacl  22218  cpmatinvcl  22219  m2cpmfo  22258  pmatcollpw3fi1lem2  22289  gausslemma2dlem1a  26868  2lgslem1b  26895  addsq2reu  26943  addsqrexnreu  26945  addsq2nreurex  26947  2sqreulem1  26949  2sqreunnlem1  26952  islnoppd  27991  outpasch  28006  hlpasch  28007  colopp  28020  colhp  28021  isinagd  28090  inaghl  28096  isleagd  28099  f1otrg  28122  usgredg4  28474  nbupgr  28601  nbumgrvtx  28603  nbgr2vtx1edg  28607  nbuhgr2vtx1edgb  28609  nbusgredgeu  28623  cusgrexilem2  28699  wlkvtxiedg  28882  elwwlks2ons3  29209  umgr2cwwkdifex  29318  1pthon2ve  29407  numclwwlk1lem2fo  29611  2ndimaxp  31872  1stpreimas  31927  swrdrn3  32119  cshwrnid  32125  gsummpt2d  32201  gsumhashmul  32208  cyc3genpmlem  32310  cyc3genpm  32311  cycpmconjs  32315  cyc3conja  32316  fldgenval  32402  dvdsruassoi  32489  dvdsruasso  32490  lsmsnidl  32509  grplsmid  32514  quslsm  32516  nsgmgc  32523  nsgqusf1olem1  32524  nsgqusf1olem2  32525  nsgqusf1olem3  32526  ghmquskerlem1  32528  elrspunidl  32546  elrspunsn  32547  mxidlprm  32586  mxidlirredi  32587  qsdrngilem  32608  ply1degltdimlem  32707  fedgmul  32716  ccfldextdgrr  32746  irngss  32751  irngnzply1lem  32754  evls1maprnss  32761  algextdeglem1  32772  ist0cld  32813  zarclsun  32850  zarclsint  32852  zarcmplem  32861  rhmpreimacn  32865  esum2d  33091  reprsuc  33627  reprpmtf1o  33638  fmlasuc  34377  fmla1  34378  satffunlem1lem2  34394  satffunlem2lem2  34397  sategoelfvb  34410  2goelgoanfmla1  34415  unblimceq0lem  35382  unblimceq0  35383  unbdqndv2  35387  knoppndvlem19  35406  aks4d1  40954  aks6d1c2p2  40957  3rspcedvd  41031  fsuppind  41162  nnn1suc  41180  sn-negex12  41289  prjspertr  41347  prjsperref  41348  prjspersym  41349  prjspvs  41352  0prjspnrel  41369  oacl2g  42080  omcl2  42083  ofoaf  42105  dfno2  42179  clsk3nimkb  42791  clsk1indlem1  42796  ntrclsiso  42818  ntrclsk2  42819  ntrclskb  42820  ntrclsk3  42821  ntrclsk13  42822  ntrclsk4  42823  imo72b2lem0  42917  imo72b2lem2  42919  imo72b2lem1  42921  imo72b2  42924  mnuprdlem4  43034  mnuunid  43036  mnurndlem2  43041  restsubel  43847  fsupdm  45558  finfdm  45562  fsetsniunop  45759  fsetsnf  45761  cfsetsnfsetf  45768  cfsetsnfsetfo  45770  2reu8i  45821  preimafvelsetpreimafv  46056  imasetpreimafvbijlemfo  46073  iccelpart  46101  fargshiftfo  46110  sprsymrelf1lem  46159  sprsymrelfo  46165  prproropf1o  46175  paireqne  46179  fmtnoodd  46201  fmtnoprmfac2lem1  46234  fmtnofac2lem  46236  fmtnofac2  46237  fmtnofac1  46238  41prothprm  46287  requad01  46289  dfodd6  46305  dfeven4  46306  opoeALTV  46351  opeoALTV  46352  nn0onn0exALTV  46367  nn0enn0exALTV  46368  nnennexALTV  46369  mogoldbblem  46388  sbgoldbst  46446  sgoldbeven3prm  46451  sbgoldbo  46455  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  evengpop3  46466  evengpoap3  46467  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  bgoldbtbndlem4  46476  bgoldbtbnd  46477  bgoldbachlt  46481  tgoldbachlt  46484  isomuspgrlem2d  46499  uspgrsprfo  46526  1odd  46581  nnsgrpnmnd  46588  rngisomring  46719  rngqiprngimfo  46786  ring2idlqus  46794  pzriprnglem10  46814  pzriprnglem11  46815  0even  46829  2even  46831  2zlidl  46832  2zrngamgm  46837  2zrngamnd  46839  2zrngagrp  46841  2zrngmmgm  46844  2zrngnmlid  46847  ply1mulgsumlem1  47067  ply1mulgsumlem2  47068  el0ldep  47147  mod0mul  47205  nn0onn0ex  47209  nn0enn0ex  47210  nnennex  47211  nnpw2p  47272  1arymaptfo  47329  2arymaptfo  47340  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  rrx2vlinest  47427  itsclquadb  47462