Theorem rspcedvd 3609

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534   ∈ wcel 2099  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061

This theorem is referenced by:  rspcime  3612  rspcedeq1vd  3614  rspcedeq2vd  3615  fsnex  7289  updjud  9970  modfzo0difsn  13957  ssnn0fi  13999  fsuppmapnn0fiubex  14006  wrdl1exs1  14616  cshimadifsn0  14834  reusq0  15462  divconjdvds  16312  2tp1odd  16349  dfgcd2  16542  fissn0dvds  16615  ncoprmlnprm  16725  dvdsprmpweq  16881  oddprmdvds  16900  prmgaplem2  17047  prmgaplcmlem2  17049  prmgaplem5  17052  prmgapprmolem  17058  fullestrcsetc  18170  equivestrcsetc  18171  fullsetcestrc  18185  isnsgrp  18711  efmndmnd  18874  smndex1mnd  18895  smndex1n0mnd  18897  mgmnsgrpex  18916  sgrpnmndex  18917  dfgrp2  18952  grplrinv  18986  grpidinv  18988  dfgrp3  19029  cycsubmcl  19191  cycsubm  19192  ghmquskerlem1  19273  ringid  20249  ringadd2  20251  ringunitnzdiv  20376  rngisomring  20445  rngqiprngimfo  21286  ring2idlqus  21294  pzriprnglem10  21476  pzriprnglem11  21477  cply1coe0bi  22290  evls1maprnss  22366  scmatid  22504  scmataddcl  22506  scmatsubcl  22507  scmatmulcl  22508  scmatrhmcl  22518  mat0scmat  22528  symgmatr01lem  22643  cpmatacl  22706  cpmatinvcl  22707  m2cpmfo  22746  pmatcollpw3fi1lem2  22777  gausslemma2dlem1a  27391  2lgslem1b  27418  addsq2reu  27466  addsqrexnreu  27468  addsq2nreurex  27470  2sqreulem1  27472  2sqreunnlem1  27475  islnoppd  28664  outpasch  28679  hlpasch  28680  colopp  28693  colhp  28694  isinagd  28763  inaghl  28769  isleagd  28772  f1otrg  28795  usgredg4  29150  nbupgr  29277  nbumgrvtx  29279  nbgr2vtx1edg  29283  nbuhgr2vtx1edgb  29285  nbusgredgeu  29299  cusgrexilem2  29375  wlkvtxiedg  29559  elwwlks2ons3  29886  umgr2cwwkdifex  29995  1pthon2ve  30084  numclwwlk1lem2fo  30288  2ndimaxp  32564  1stpreimas  32617  swrdrn3  32822  cshwrnid  32828  gsummpt2d  32921  gsumhashmul  32929  cyc3genpmlem  33033  cyc3genpm  33034  cycpmconjs  33038  cyc3conja  33039  erlbrd  33123  erler  33125  rloccring  33130  fldgenval  33167  dvdsruassoi  33265  dvdsruasso  33266  lsmsnidl  33280  grplsmid  33285  quslsm  33286  nsgmgc  33293  nsgqusf1olem1  33294  nsgqusf1olem2  33295  nsgqusf1olem3  33296  elrspunidl  33309  elrspunsn  33310  mxidlprm  33351  mxidlirredi  33352  qsdrngilem  33375  1arithidom  33418  fedgmul  33532  ccfldextdgrr  33564  irngss  33569  irngnzply1lem  33572  constrsslem  33613  constrconj  33617  ist0cld  33661  zarclsun  33698  zarclsint  33700  zarcmplem  33709  rhmpreimacn  33713  esum2d  33939  reprsuc  34474  reprpmtf1o  34485  fmlasuc  35227  fmla1  35228  satffunlem1lem2  35244  satffunlem2lem2  35247  sategoelfvb  35260  2goelgoanfmla1  35265  unblimceq0lem  36222  unblimceq0  36223  unbdqndv2  36227  knoppndvlem19  36246  aks4d1  41801  primrootsunit1  41809  primrootscoprmpow  41811  primrootscoprbij  41814  remexz  41816  aks6d1c2p2  41831  hashscontpow1  41833  aks6d1c6isolem1  41886  aks6d1c6lem5  41889  3rspcedvd  41959  oacl2g  43033  omcl2  43036  ofoaf  43058  dfno2  43132  clsk3nimkb  43744  clsk1indlem1  43749  ntrclsiso  43771  ntrclsk2  43772  ntrclskb  43773  ntrclsk3  43774  ntrclsk13  43775  ntrclsk4  43776  imo72b2lem0  43869  imo72b2lem2  43871  imo72b2lem1  43873  imo72b2  43876  mnuprdlem4  43986  mnuunid  43988  mnurndlem2  43993  restsubel  44794  fsupdm  46499  finfdm  46503  fsetsniunop  46700  fsetsnf  46702  cfsetsnfsetf  46709  cfsetsnfsetfo  46711  2reu8i  46762  preimafvelsetpreimafv  46996  imasetpreimafvbijlemfo  47013  iccelpart  47041  fargshiftfo  47050  sprsymrelf1lem  47099  sprsymrelfo  47105  prproropf1o  47115  paireqne  47119  fmtnoodd  47141  fmtnoprmfac2lem1  47174  fmtnofac2lem  47176  fmtnofac2  47177  fmtnofac1  47178  41prothprm  47227  requad01  47229  dfodd6  47245  dfeven4  47246  opoeALTV  47291  opeoALTV  47292  nn0onn0exALTV  47307  nn0enn0exALTV  47308  nnennexALTV  47309  mogoldbblem  47328  sbgoldbst  47386  sgoldbeven3prm  47391  sbgoldbo  47395  nnsum3primesgbe  47400  nnsum4primesodd  47404  nnsum4primesoddALTV  47405  evengpop3  47406  evengpoap3  47407  nnsum4primeseven  47408  nnsum4primesevenALTV  47409  wtgoldbnnsum4prm  47410  bgoldbnnsum3prm  47412  bgoldbtbndlem4  47416  bgoldbtbnd  47417  bgoldbachlt  47421  tgoldbachlt  47424  clnbgrgrimlem  47516  uspgrsprfo  47561  1odd  47584  nnsgrpnmnd  47591  0even  47650  2even  47652  2zlidl  47653  2zrngamgm  47658  2zrngamnd  47660  2zrngagrp  47662  2zrngmmgm  47665  2zrngnmlid  47668  ply1mulgsumlem1  47805  ply1mulgsumlem2  47806  el0ldep  47885  mod0mul  47943  nn0onn0ex  47947  nn0enn0ex  47948  nnennex  47949  nnpw2p  48010  1arymaptfo  48067  2arymaptfo  48078  eenglngeehlnmlem1  48161  eenglngeehlnmlem2  48162  rrx2vlinest  48165  itsclquadb  48200