Theorem rspcedvd 3614

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071

This theorem is referenced by:  rspcime  3616  rspcedeq1vd  3618  rspcedeq2vd  3619  elpr2elpr  4869  prproe  4906  fsnex  7280  fsetfocdm  8854  updjud  9928  negfi  12162  elpq  12958  reltre  13318  rpltrp  13319  reltxrnmnf  13320  modmuladd  13877  modmuladdnn0  13879  modfzo0difsn  13907  ssnn0fi  13949  fsuppmapnn0fiubex  13956  wrdl1exs1  14562  cshimadifsn0  14780  reusq0  15408  divconjdvds  16257  2tp1odd  16294  dfgcd2  16487  fissn0dvds  16555  ncoprmlnprm  16663  dvdsprmpweq  16816  oddprmdvds  16835  prmgaplem2  16982  prmgaplcmlem2  16984  prmgaplem5  16987  prmgapprmolem  16993  fullestrcsetc  18102  equivestrcsetc  18103  fullsetcestrc  18117  isnsgrp  18613  efmndmnd  18769  smndex1mnd  18790  smndex1n0mnd  18792  mgmnsgrpex  18811  sgrpnmndex  18812  dfgrp2  18846  grplrinv  18880  grpidinv  18882  dfgrp3  18921  cycsubmcl  19077  cycsubm  19078  ringid  20090  ringadd2  20092  ringunitnzdiv  20211  cply1coe0bi  21823  scmatid  22015  scmataddcl  22017  scmatsubcl  22018  scmatmulcl  22019  scmatrhmcl  22029  mat0scmat  22039  symgmatr01lem  22154  cpmatacl  22217  cpmatinvcl  22218  m2cpmfo  22257  pmatcollpw3fi1lem2  22288  gausslemma2dlem1a  26865  2lgslem1b  26892  addsq2reu  26940  addsqrexnreu  26942  addsq2nreurex  26944  2sqreulem1  26946  2sqreunnlem1  26949  islnoppd  27988  outpasch  28003  hlpasch  28004  colopp  28017  colhp  28018  isinagd  28087  inaghl  28093  isleagd  28096  f1otrg  28119  usgredg4  28471  nbupgr  28598  nbumgrvtx  28600  nbgr2vtx1edg  28604  nbuhgr2vtx1edgb  28606  nbusgredgeu  28620  cusgrexilem2  28696  wlkvtxiedg  28879  elwwlks2ons3  29206  umgr2cwwkdifex  29315  1pthon2ve  29404  numclwwlk1lem2fo  29608  2ndimaxp  31867  1stpreimas  31922  swrdrn3  32114  cshwrnid  32120  gsummpt2d  32196  gsumhashmul  32203  cyc3genpmlem  32305  cyc3genpm  32306  cycpmconjs  32310  cyc3conja  32311  fldgenval  32397  dvdsruassoi  32484  dvdsruasso  32485  lsmsnidl  32504  grplsmid  32509  quslsm  32511  nsgmgc  32518  nsgqusf1olem1  32519  nsgqusf1olem2  32520  nsgqusf1olem3  32521  ghmquskerlem1  32523  elrspunidl  32541  elrspunsn  32542  mxidlprm  32581  mxidlirredi  32582  qsdrngilem  32603  ply1degltdimlem  32702  fedgmul  32711  ccfldextdgrr  32741  irngss  32746  irngnzply1lem  32749  evls1maprnss  32756  algextdeglem1  32767  ist0cld  32808  zarclsun  32845  zarclsint  32847  zarcmplem  32856  rhmpreimacn  32860  esum2d  33086  reprsuc  33622  reprpmtf1o  33633  fmlasuc  34372  fmla1  34373  satffunlem1lem2  34389  satffunlem2lem2  34392  sategoelfvb  34405  2goelgoanfmla1  34410  unblimceq0lem  35377  unblimceq0  35378  unbdqndv2  35382  knoppndvlem19  35401  aks4d1  40949  aks6d1c2p2  40952  3rspcedvd  41033  fsuppind  41164  nnn1suc  41182  sn-negex12  41290  prjspertr  41348  prjsperref  41349  prjspersym  41350  prjspvs  41353  0prjspnrel  41370  oacl2g  42070  omcl2  42073  ofoaf  42095  dfno2  42169  clsk3nimkb  42781  clsk1indlem1  42786  ntrclsiso  42808  ntrclsk2  42809  ntrclskb  42810  ntrclsk3  42811  ntrclsk13  42812  ntrclsk4  42813  imo72b2lem0  42907  imo72b2lem2  42909  imo72b2lem1  42911  imo72b2  42914  mnuprdlem4  43024  mnuunid  43026  mnurndlem2  43031  restsubel  43837  fsupdm  45548  finfdm  45552  fsetsniunop  45749  fsetsnf  45751  cfsetsnfsetf  45758  cfsetsnfsetfo  45760  2reu8i  45811  preimafvelsetpreimafv  46046  imasetpreimafvbijlemfo  46063  iccelpart  46091  fargshiftfo  46100  sprsymrelf1lem  46149  sprsymrelfo  46155  prproropf1o  46165  paireqne  46169  fmtnoodd  46191  fmtnoprmfac2lem1  46224  fmtnofac2lem  46226  fmtnofac2  46227  fmtnofac1  46228  41prothprm  46277  requad01  46279  dfodd6  46295  dfeven4  46296  opoeALTV  46341  opeoALTV  46342  nn0onn0exALTV  46357  nn0enn0exALTV  46358  nnennexALTV  46359  mogoldbblem  46378  sbgoldbst  46436  sgoldbeven3prm  46441  sbgoldbo  46445  nnsum3primesgbe  46450  nnsum4primesodd  46454  nnsum4primesoddALTV  46455  evengpop3  46456  evengpoap3  46457  nnsum4primeseven  46458  nnsum4primesevenALTV  46459  wtgoldbnnsum4prm  46460  bgoldbnnsum3prm  46462  bgoldbtbndlem4  46466  bgoldbtbnd  46467  bgoldbachlt  46471  tgoldbachlt  46474  isomuspgrlem2d  46489  uspgrsprfo  46516  1odd  46571  nnsgrpnmnd  46578  rngisomring  46709  rngqiprngimfo  46776  ring2idlqus  46784  pzriprnglem10  46804  pzriprnglem11  46805  0even  46819  2even  46821  2zlidl  46822  2zrngamgm  46827  2zrngamnd  46829  2zrngagrp  46831  2zrngmmgm  46834  2zrngnmlid  46837  ply1mulgsumlem1  47057  ply1mulgsumlem2  47058  el0ldep  47137  mod0mul  47195  nn0onn0ex  47199  nn0enn0ex  47200  nnennex  47201  nnpw2p  47262  1arymaptfo  47319  2arymaptfo  47330  eenglngeehlnmlem1  47413  eenglngeehlnmlem2  47414  rrx2vlinest  47417  itsclquadb  47452