Theorem rspcedvd 3584

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090

This theorem is referenced by:  rspcime  3587  fsnex  7283  updjud  9921  modfzo0difsn  13981  ssnn0fi  14023  fsuppmapnn0fiubex  14030  tpfo  14539  wrdl1exs1  14653  cshimadifsn0  14869  reusq0  15518  divconjdvds  16374  2tp1odd  16411  dfgcd2  16605  fissn0dvds  16678  ncoprmlnprm  16788  dvdsprmpweq  16945  oddprmdvds  16964  prmgaplem2  17111  prmgaplcmlem2  17113  prmgaplem5  17116  prmgapprmolem  17122  fullestrcsetc  18208  equivestrcsetc  18209  fullsetcestrc  18223  isnsgrp  18782  efmndmnd  18949  smndex1mnd  18973  smndex1n0mnd  18975  mgmnsgrpex  18994  sgrpnmndex  18995  dfgrp2  19030  grplrinv  19064  grpidinv  19066  dfgrp3  19106  cycsubmcl  19273  cycsubm  19274  ghmquskerlem1  19354  ringid  20358  ringadd2  20360  ringunitnzdiv  20481  rngisomring  20550  rngqiprngimfo  21422  ring2idlqus  21430  pzriprnglem10  21621  pzriprnglem11  21622  cply1coe0bi  22443  evls1maprnss  22519  scmatid  22652  scmataddcl  22654  scmatsubcl  22655  scmatmulcl  22656  scmatrhmcl  22666  mat0scmat  22676  symgmatr01lem  22791  cpmatacl  22854  cpmatinvcl  22855  m2cpmfo  22894  pmatcollpw3fi1lem2  22925  gausslemma2dlem1a  27507  2lgslem1b  27534  addsq2reu  27582  addsqrexnreu  27584  addsq2nreurex  27586  2sqreulem1  27588  2sqreunnlem1  27591  islnoppd  28999  outpasch  29015  hlpasch  29016  colopp  29029  colhp  29030  isinagd  29134  inaghl  29140  isleagd  29143  f1otrg  29198  usgredg4  29545  nbupgr  29672  nbumgrvtx  29674  nbgr2vtx1edg  29678  nbuhgr2vtx1edgb  29680  nbusgredgeu  29694  cusgrexilem2  29770  wlkvtxiedg  29952  elwwlks2ons3  30282  umgr2cwwkdifex  30394  1pthon2ve  30483  numclwwlk1lem2fo  30687  2ndimaxp  32969  1stpreimas  33029  swrdrn3  33253  cshwrnid  33259  gsummpt2d  33347  gsumhashmul  33365  cyc3genpmlem  33449  cyc3genpm  33450  cycpmconjs  33454  cyc3conja  33455  elrgspnlem1  33540  elrgspnsubrunlem2  33546  erlbrd  33561  erler  33563  rloccring  33569  rlocisunit  33574  fldgenval  33611  dvdsruassoi  33675  dvdsruasso  33676  lsmsnidl  33688  grplsmid  33691  quslsm  33692  nsgmgc  33699  nsgqusf1olem1  33700  nsgqusf1olem2  33701  nsgqusf1olem3  33702  elrspunidl  33714  elrspunsn  33715  mxidlprm  33731  qsdrngilem  33754  1arithidom  33805  fedgmul  33999  ccfldextdgrr  34040  fldextrspunlsplem  34041  irngss  34055  irngnzply1lem  34058  constrsslem  34109  constrconj  34113  constrfiss  34119  constrllcllem  34120  constrlccllem  34121  constrcccllem  34122  nn0constr  34129  ist0cld  34201  zarclsun  34238  zarclsint  34240  zarcmplem  34249  rhmpreimacn  34253  esum2d  34461  reprsuc  34980  reprpmtf1o  34991  fmlasuc  35856  fmla1  35857  satffunlem1lem2  35873  satffunlem2lem2  35876  sategoelfvb  35889  2goelgoanfmla1  35894  unblimceq0lem  37073  unblimceq0  37074  unbdqndv2  37078  knoppndvlem19  37097  aks4d1  42834  primrootsunit1  42842  primrootscoprmpow  42844  primrootscoprbij  42847  remexz  42849  aks6d1c2p2  42864  hashscontpow1  42866  aks6d1c6isolem1  42919  aks6d1c6lem5  42922  unitscyglem5  42944  aks5lem8  42946  3rspcedvd  42965  oacl2g  44037  omcl2  44040  ofoaf  44062  dfno2  44134  clsk3nimkb  44746  clsk1indlem1  44751  ntrclsiso  44773  ntrclsk2  44774  ntrclskb  44775  ntrclsk3  44776  ntrclsk13  44777  ntrclsk4  44778  imo72b2lem0  44871  imo72b2lem2  44873  imo72b2lem1  44875  imo72b2  44878  mnuprdlem4  44965  mnuunid  44967  mnurndlem2  44972  restsubel  45851  fsupdm  47536  finfdm  47540  fsetsniunop  47763  fsetsnf  47765  cfsetsnfsetf  47772  cfsetsnfsetfo  47774  2reu8i  47827  mod0mul  48076  nndivides2  48098  preimafvelsetpreimafv  48114  imasetpreimafvbijlemfo  48131  iccelpart  48159  fargshiftfo  48168  sprsymrelf1lem  48217  sprsymrelfo  48223  prproropf1o  48233  paireqne  48237  nprmmul3  48255  fmtnoodd  48262  fmtnoprmfac2lem1  48295  fmtnofac2lem  48297  fmtnofac2  48298  fmtnofac1  48299  41prothprm  48348  requad01  48363  dfodd6  48379  dfeven4  48380  opoeALTV  48425  opeoALTV  48426  nn0onn0exALTV  48441  nn0enn0exALTV  48442  nnennexALTV  48443  mogoldbblem  48462  sbgoldbst  48520  sgoldbeven3prm  48525  sbgoldbo  48529  nnsum3primesgbe  48534  nnsum4primesodd  48538  nnsum4primesoddALTV  48539  evengpop3  48540  evengpoap3  48541  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  wtgoldbnnsum4prm  48544  bgoldbnnsum3prm  48546  bgoldbtbndlem4  48550  bgoldbtbnd  48551  bgoldbachlt  48555  tgoldbachlt  48558  predgclnbgrel  48581  clnbgredg  48582  clnbgrgrimlem  48675  grlimgredgex  48742  gpgprismgriedgdmss  48794  gpgedgvtx0  48803  gpgedgiov  48807  gpg3kgrtriexlem6  48830  gpg3kgrtriex  48831  uspgrsprfo  48890  1odd  48913  nnsgrpnmnd  48920  0even  48979  2even  48981  2zlidl  48982  2zrngamgm  48987  2zrngamnd  48989  2zrngagrp  48991  2zrngmmgm  48994  2zrngnmlid  48997  ply1mulgsumlem1  49143  ply1mulgsumlem2  49144  el0ldep  49223  nn0onn0ex  49280  nn0enn0ex  49281  nnennex  49282  nnpw2p  49343  1arymaptfo  49400  2arymaptfo  49411  eenglngeehlnmlem1  49494  eenglngeehlnmlem2  49495  rrx2vlinest  49498  itsclquadb  49533  iunlub  49576  iinglb  49577