Theorem rspcedvd 3583

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086

This theorem is referenced by:  rspcime  3586  fsnex  7263  updjud  9889  modfzo0difsn  13953  ssnn0fi  13995  fsuppmapnn0fiubex  14002  tpfo  14510  wrdl1exs1  14624  cshimadifsn0  14840  reusq0  15475  divconjdvds  16332  2tp1odd  16369  dfgcd2  16563  fissn0dvds  16636  ncoprmlnprm  16746  dvdsprmpweq  16903  oddprmdvds  16922  prmgaplem2  17069  prmgaplcmlem2  17071  prmgaplem5  17074  prmgapprmolem  17080  fullestrcsetc  18166  equivestrcsetc  18167  fullsetcestrc  18181  isnsgrp  18740  efmndmnd  18906  smndex1mnd  18930  smndex1n0mnd  18932  mgmnsgrpex  18951  sgrpnmndex  18952  dfgrp2  18987  grplrinv  19021  grpidinv  19023  dfgrp3  19064  cycsubmcl  19225  cycsubm  19226  ghmquskerlem1  19306  ringid  20303  ringadd2  20305  ringunitnzdiv  20426  rngisomring  20495  rngqiprngimfo  21351  ring2idlqus  21359  pzriprnglem10  21522  pzriprnglem11  21523  cply1coe0bi  22345  evls1maprnss  22421  scmatid  22554  scmataddcl  22556  scmatsubcl  22557  scmatmulcl  22558  scmatrhmcl  22568  mat0scmat  22578  symgmatr01lem  22693  cpmatacl  22756  cpmatinvcl  22757  m2cpmfo  22796  pmatcollpw3fi1lem2  22827  gausslemma2dlem1a  27406  2lgslem1b  27433  addsq2reu  27481  addsqrexnreu  27483  addsq2nreurex  27485  2sqreulem1  27487  2sqreunnlem1  27490  islnoppd  28886  outpasch  28901  hlpasch  28902  colopp  28915  colhp  28916  isinagd  28985  inaghl  28991  isleagd  28994  f1otrg  29017  usgredg4  29364  nbupgr  29491  nbumgrvtx  29493  nbgr2vtx1edg  29497  nbuhgr2vtx1edgb  29499  nbusgredgeu  29513  cusgrexilem2  29589  wlkvtxiedg  29771  elwwlks2ons3  30101  umgr2cwwkdifex  30213  1pthon2ve  30302  numclwwlk1lem2fo  30506  2ndimaxp  32798  1stpreimas  32858  swrdrn3  33094  cshwrnid  33100  gsummpt2d  33190  gsumhashmul  33208  cyc3genpmlem  33292  cyc3genpm  33293  cycpmconjs  33297  cyc3conja  33298  elrgspnlem1  33384  elrgspnsubrunlem2  33390  erlbrd  33405  erler  33407  rloccring  33413  rlocisunit  33418  fldgenval  33460  dvdsruassoi  33531  dvdsruasso  33532  lsmsnidl  33546  grplsmid  33551  quslsm  33552  nsgmgc  33559  nsgqusf1olem1  33560  nsgqusf1olem2  33561  nsgqusf1olem3  33562  elrspunidl  33575  elrspunsn  33576  mxidlprm  33619  qsdrngilem  33643  1arithidom  33694  fedgmul  33889  ccfldextdgrr  33930  fldextrspunlsplem  33931  irngss  33945  irngnzply1lem  33948  constrsslem  33999  constrconj  34003  constrfiss  34009  constrllcllem  34010  constrlccllem  34011  constrcccllem  34012  nn0constr  34019  ist0cld  34091  zarclsun  34128  zarclsint  34130  zarcmplem  34139  rhmpreimacn  34143  esum2d  34351  reprsuc  34873  reprpmtf1o  34884  fmlasuc  35700  fmla1  35701  satffunlem1lem2  35717  satffunlem2lem2  35720  sategoelfvb  35733  2goelgoanfmla1  35738  unblimceq0lem  36908  unblimceq0  36909  unbdqndv2  36913  knoppndvlem19  36932  aks4d1  42670  primrootsunit1  42678  primrootscoprmpow  42680  primrootscoprbij  42683  remexz  42685  aks6d1c2p2  42700  hashscontpow1  42702  aks6d1c6isolem1  42755  aks6d1c6lem5  42758  unitscyglem5  42780  aks5lem8  42782  3rspcedvd  42799  oacl2g  43871  omcl2  43874  ofoaf  43896  dfno2  43968  clsk3nimkb  44580  clsk1indlem1  44585  ntrclsiso  44607  ntrclsk2  44608  ntrclskb  44609  ntrclsk3  44610  ntrclsk13  44611  ntrclsk4  44612  imo72b2lem0  44705  imo72b2lem2  44707  imo72b2lem1  44709  imo72b2  44712  mnuprdlem4  44815  mnuunid  44817  mnurndlem2  44822  restsubel  45695  fsupdm  47380  finfdm  47384  fsetsniunop  47607  fsetsnf  47609  cfsetsnfsetf  47616  cfsetsnfsetfo  47618  2reu8i  47671  mod0mul  47920  nndivides2  47942  preimafvelsetpreimafv  47958  imasetpreimafvbijlemfo  47975  iccelpart  48003  fargshiftfo  48012  sprsymrelf1lem  48061  sprsymrelfo  48067  prproropf1o  48077  paireqne  48081  nprmmul3  48099  fmtnoodd  48106  fmtnoprmfac2lem1  48139  fmtnofac2lem  48141  fmtnofac2  48142  fmtnofac1  48143  41prothprm  48192  requad01  48207  dfodd6  48223  dfeven4  48224  opoeALTV  48269  opeoALTV  48270  nn0onn0exALTV  48285  nn0enn0exALTV  48286  nnennexALTV  48287  mogoldbblem  48306  sbgoldbst  48364  sgoldbeven3prm  48369  sbgoldbo  48373  nnsum3primesgbe  48378  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  evengpop3  48384  evengpoap3  48385  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  wtgoldbnnsum4prm  48388  bgoldbnnsum3prm  48390  bgoldbtbndlem4  48394  bgoldbtbnd  48395  bgoldbachlt  48399  tgoldbachlt  48402  predgclnbgrel  48425  clnbgredg  48426  clnbgrgrimlem  48519  grlimgredgex  48586  gpgprismgriedgdmss  48638  gpgedgvtx0  48647  gpgedgiov  48651  gpg3kgrtriexlem6  48674  gpg3kgrtriex  48675  uspgrsprfo  48734  1odd  48757  nnsgrpnmnd  48764  0even  48823  2even  48825  2zlidl  48826  2zrngamgm  48831  2zrngamnd  48833  2zrngagrp  48835  2zrngmmgm  48838  2zrngnmlid  48841  ply1mulgsumlem1  48972  ply1mulgsumlem2  48973  el0ldep  49052  nn0onn0ex  49109  nn0enn0ex  49110  nnennex  49111  nnpw2p  49172  1arymaptfo  49229  2arymaptfo  49240  eenglngeehlnmlem1  49323  eenglngeehlnmlem2  49324  rrx2vlinest  49327  itsclquadb  49362  iunlub  49406  iinglb  49407