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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057

This theorem is referenced by:  rspcime  3582  rspcedeq1vd  3584  rspcedeq2vd  3585  fsnex  7217  updjud  9824  modfzo0difsn  13847  ssnn0fi  13889  fsuppmapnn0fiubex  13896  tpfo  14404  wrdl1exs1  14518  cshimadifsn0  14734  reusq0  15369  divconjdvds  16223  2tp1odd  16260  dfgcd2  16454  fissn0dvds  16527  ncoprmlnprm  16636  dvdsprmpweq  16793  oddprmdvds  16812  prmgaplem2  16959  prmgaplcmlem2  16961  prmgaplem5  16964  prmgapprmolem  16970  fullestrcsetc  18054  equivestrcsetc  18055  fullsetcestrc  18069  isnsgrp  18628  efmndmnd  18794  smndex1mnd  18815  smndex1n0mnd  18817  mgmnsgrpex  18836  sgrpnmndex  18837  dfgrp2  18872  grplrinv  18906  grpidinv  18908  dfgrp3  18949  cycsubmcl  19111  cycsubm  19112  ghmquskerlem1  19193  ringid  20190  ringadd2  20192  ringunitnzdiv  20314  rngisomring  20383  rngqiprngimfo  21236  ring2idlqus  21244  pzriprnglem10  21425  pzriprnglem11  21426  cply1coe0bi  22215  evls1maprnss  22291  scmatid  22427  scmataddcl  22429  scmatsubcl  22430  scmatmulcl  22431  scmatrhmcl  22441  mat0scmat  22451  symgmatr01lem  22566  cpmatacl  22629  cpmatinvcl  22630  m2cpmfo  22669  pmatcollpw3fi1lem2  22700  gausslemma2dlem1a  27301  2lgslem1b  27328  addsq2reu  27376  addsqrexnreu  27378  addsq2nreurex  27380  2sqreulem1  27382  2sqreunnlem1  27385  islnoppd  28716  outpasch  28731  hlpasch  28732  colopp  28745  colhp  28746  isinagd  28815  inaghl  28821  isleagd  28824  f1otrg  28847  usgredg4  29193  nbupgr  29320  nbumgrvtx  29322  nbgr2vtx1edg  29326  nbuhgr2vtx1edgb  29328  nbusgredgeu  29342  cusgrexilem2  29418  wlkvtxiedg  29601  elwwlks2ons3  29931  umgr2cwwkdifex  30040  1pthon2ve  30129  numclwwlk1lem2fo  30333  2ndimaxp  32623  1stpreimas  32682  swrdrn3  32931  cshwrnid  32937  gsummpt2d  33024  gsumhashmul  33036  cyc3genpmlem  33115  cyc3genpm  33116  cycpmconjs  33120  cyc3conja  33121  elrgspnlem1  33204  elrgspnsubrunlem2  33210  erlbrd  33225  erler  33227  rloccring  33232  fldgenval  33273  dvdsruassoi  33344  dvdsruasso  33345  lsmsnidl  33359  grplsmid  33364  quslsm  33365  nsgmgc  33372  nsgqusf1olem1  33373  nsgqusf1olem2  33374  nsgqusf1olem3  33375  elrspunidl  33388  elrspunsn  33389  mxidlprm  33430  mxidlirredi  33431  qsdrngilem  33454  1arithidom  33497  fedgmul  33639  ccfldextdgrr  33680  fldextrspunlsplem  33681  irngss  33695  irngnzply1lem  33698  constrsslem  33749  constrconj  33753  constrfiss  33759  constrllcllem  33760  constrlccllem  33761  constrcccllem  33762  nn0constr  33769  ist0cld  33841  zarclsun  33878  zarclsint  33880  zarcmplem  33889  rhmpreimacn  33893  esum2d  34101  reprsuc  34623  reprpmtf1o  34634  fmlasuc  35418  fmla1  35419  satffunlem1lem2  35435  satffunlem2lem2  35438  sategoelfvb  35451  2goelgoanfmla1  35456  unblimceq0lem  36539  unblimceq0  36540  unbdqndv2  36544  knoppndvlem19  36563  aks4d1  42121  primrootsunit1  42129  primrootscoprmpow  42131  primrootscoprbij  42134  remexz  42136  aks6d1c2p2  42151  hashscontpow1  42153  aks6d1c6isolem1  42206  aks6d1c6lem5  42209  unitscyglem5  42231  aks5lem8  42233  3rspcedvd  42247  oacl2g  43362  omcl2  43365  ofoaf  43387  dfno2  43460  clsk3nimkb  44072  clsk1indlem1  44077  ntrclsiso  44099  ntrclsk2  44100  ntrclskb  44101  ntrclsk3  44102  ntrclsk13  44103  ntrclsk4  44104  imo72b2lem0  44197  imo72b2lem2  44199  imo72b2lem1  44201  imo72b2  44204  mnuprdlem4  44307  mnuunid  44309  mnurndlem2  44314  restsubel  45189  fsupdm  46879  finfdm  46883  fsetsniunop  47079  fsetsnf  47081  cfsetsnfsetf  47088  cfsetsnfsetfo  47090  2reu8i  47143  mod0mul  47386  preimafvelsetpreimafv  47418  imasetpreimafvbijlemfo  47435  iccelpart  47463  fargshiftfo  47472  sprsymrelf1lem  47521  sprsymrelfo  47527  prproropf1o  47537  paireqne  47541  fmtnoodd  47563  fmtnoprmfac2lem1  47596  fmtnofac2lem  47598  fmtnofac2  47599  fmtnofac1  47600  41prothprm  47649  requad01  47651  dfodd6  47667  dfeven4  47668  opoeALTV  47713  opeoALTV  47714  nn0onn0exALTV  47729  nn0enn0exALTV  47730  nnennexALTV  47731  mogoldbblem  47750  sbgoldbst  47808  sgoldbeven3prm  47813  sbgoldbo  47817  nnsum3primesgbe  47822  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  evengpop3  47828  evengpoap3  47829  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  wtgoldbnnsum4prm  47832  bgoldbnnsum3prm  47834  bgoldbtbndlem4  47838  bgoldbtbnd  47839  bgoldbachlt  47843  tgoldbachlt  47846  predgclnbgrel  47869  clnbgredg  47870  clnbgrgrimlem  47963  grlimgredgex  48030  gpgprismgriedgdmss  48082  gpgedgvtx0  48091  gpgedgiov  48095  gpg3kgrtriexlem6  48118  gpg3kgrtriex  48119  uspgrsprfo  48178  1odd  48201  nnsgrpnmnd  48208  0even  48267  2even  48269  2zlidl  48270  2zrngamgm  48275  2zrngamnd  48277  2zrngagrp  48279  2zrngmmgm  48282  2zrngnmlid  48285  ply1mulgsumlem1  48417  ply1mulgsumlem2  48418  el0ldep  48497  nn0onn0ex  48554  nn0enn0ex  48555  nnennex  48556  nnpw2p  48617  1arymaptfo  48674  2arymaptfo  48685  eenglngeehlnmlem1  48768  eenglngeehlnmlem2  48769  rrx2vlinest  48772  itsclquadb  48807  iunlub  48851  iinglb  48852