Theorem rspcedvd 3624

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071

This theorem is referenced by:  rspcime  3627  rspcedeq1vd  3629  rspcedeq2vd  3630  fsnex  7303  updjud  9974  modfzo0difsn  13984  ssnn0fi  14026  fsuppmapnn0fiubex  14033  tpfo  14539  wrdl1exs1  14651  cshimadifsn0  14869  reusq0  15501  divconjdvds  16352  2tp1odd  16389  dfgcd2  16583  fissn0dvds  16656  ncoprmlnprm  16765  dvdsprmpweq  16922  oddprmdvds  16941  prmgaplem2  17088  prmgaplcmlem2  17090  prmgaplem5  17093  prmgapprmolem  17099  fullestrcsetc  18196  equivestrcsetc  18197  fullsetcestrc  18211  isnsgrp  18736  efmndmnd  18902  smndex1mnd  18923  smndex1n0mnd  18925  mgmnsgrpex  18944  sgrpnmndex  18945  dfgrp2  18980  grplrinv  19014  grpidinv  19016  dfgrp3  19057  cycsubmcl  19219  cycsubm  19220  ghmquskerlem1  19301  ringid  20271  ringadd2  20273  ringunitnzdiv  20398  rngisomring  20467  rngqiprngimfo  21311  ring2idlqus  21319  pzriprnglem10  21501  pzriprnglem11  21502  cply1coe0bi  22306  evls1maprnss  22382  scmatid  22520  scmataddcl  22522  scmatsubcl  22523  scmatmulcl  22524  scmatrhmcl  22534  mat0scmat  22544  symgmatr01lem  22659  cpmatacl  22722  cpmatinvcl  22723  m2cpmfo  22762  pmatcollpw3fi1lem2  22793  gausslemma2dlem1a  27409  2lgslem1b  27436  addsq2reu  27484  addsqrexnreu  27486  addsq2nreurex  27488  2sqreulem1  27490  2sqreunnlem1  27493  islnoppd  28748  outpasch  28763  hlpasch  28764  colopp  28777  colhp  28778  isinagd  28847  inaghl  28853  isleagd  28856  f1otrg  28879  usgredg4  29234  nbupgr  29361  nbumgrvtx  29363  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  nbusgredgeu  29383  cusgrexilem2  29459  wlkvtxiedg  29643  elwwlks2ons3  29975  umgr2cwwkdifex  30084  1pthon2ve  30173  numclwwlk1lem2fo  30377  2ndimaxp  32656  1stpreimas  32715  swrdrn3  32940  cshwrnid  32946  gsummpt2d  33052  gsumhashmul  33064  cyc3genpmlem  33171  cyc3genpm  33172  cycpmconjs  33176  cyc3conja  33177  elrgspnlem1  33246  elrgspnsubrunlem2  33252  erlbrd  33267  erler  33269  rloccring  33274  fldgenval  33314  dvdsruassoi  33412  dvdsruasso  33413  lsmsnidl  33427  grplsmid  33432  quslsm  33433  nsgmgc  33440  nsgqusf1olem1  33441  nsgqusf1olem2  33442  nsgqusf1olem3  33443  elrspunidl  33456  elrspunsn  33457  mxidlprm  33498  mxidlirredi  33499  qsdrngilem  33522  1arithidom  33565  fedgmul  33682  ccfldextdgrr  33722  fldextrspunlsplem  33723  irngss  33737  irngnzply1lem  33740  constrsslem  33782  constrconj  33786  ist0cld  33832  zarclsun  33869  zarclsint  33871  zarcmplem  33880  rhmpreimacn  33884  esum2d  34094  reprsuc  34630  reprpmtf1o  34641  fmlasuc  35391  fmla1  35392  satffunlem1lem2  35408  satffunlem2lem2  35411  sategoelfvb  35424  2goelgoanfmla1  35429  unblimceq0lem  36507  unblimceq0  36508  unbdqndv2  36512  knoppndvlem19  36531  aks4d1  42090  primrootsunit1  42098  primrootscoprmpow  42100  primrootscoprbij  42103  remexz  42105  aks6d1c2p2  42120  hashscontpow1  42122  aks6d1c6isolem1  42175  aks6d1c6lem5  42178  unitscyglem5  42200  aks5lem8  42202  3rspcedvd  42254  oacl2g  43343  omcl2  43346  ofoaf  43368  dfno2  43441  clsk3nimkb  44053  clsk1indlem1  44058  ntrclsiso  44080  ntrclsk2  44081  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  ntrclsk4  44085  imo72b2lem0  44178  imo72b2lem2  44180  imo72b2lem1  44182  imo72b2  44185  mnuprdlem4  44294  mnuunid  44296  mnurndlem2  44301  restsubel  45158  fsupdm  46857  finfdm  46861  fsetsniunop  47061  fsetsnf  47063  cfsetsnfsetf  47070  cfsetsnfsetfo  47072  2reu8i  47125  preimafvelsetpreimafv  47375  imasetpreimafvbijlemfo  47392  iccelpart  47420  fargshiftfo  47429  sprsymrelf1lem  47478  sprsymrelfo  47484  prproropf1o  47494  paireqne  47498  fmtnoodd  47520  fmtnoprmfac2lem1  47553  fmtnofac2lem  47555  fmtnofac2  47556  fmtnofac1  47557  41prothprm  47606  requad01  47608  dfodd6  47624  dfeven4  47625  opoeALTV  47670  opeoALTV  47671  nn0onn0exALTV  47686  nn0enn0exALTV  47687  nnennexALTV  47688  mogoldbblem  47707  sbgoldbst  47765  sgoldbeven3prm  47770  sbgoldbo  47774  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  evengpop3  47785  evengpoap3  47786  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem4  47795  bgoldbtbnd  47796  bgoldbachlt  47800  tgoldbachlt  47803  predgclnbgrel  47825  clnbgredg  47826  clnbgrgrimlem  47901  gpgedgvtx0  48019  gpg3kgrtriexlem6  48044  gpg3kgrtriex  48045  uspgrsprfo  48064  1odd  48087  nnsgrpnmnd  48094  0even  48153  2even  48155  2zlidl  48156  2zrngamgm  48161  2zrngamnd  48163  2zrngagrp  48165  2zrngmmgm  48168  2zrngnmlid  48171  ply1mulgsumlem1  48303  ply1mulgsumlem2  48304  el0ldep  48383  mod0mul  48440  nn0onn0ex  48444  nn0enn0ex  48445  nnennex  48446  nnpw2p  48507  1arymaptfo  48564  2arymaptfo  48575  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrx2vlinest  48662  itsclquadb  48697