Theorem rspcedvd 3537

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1508   ∈ wcel 2051  ∃wrex 3084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-ral 3088  df-rex 3089  df-v 3412

This theorem is referenced by:  rspcedeq1vd  3539  rspcedeq2vd  3540  clel5OLD  3567  elpr2elpr  4670  prproe  4707  fsnex  6863  updjud  9156  negfi  11389  fiminreOLD  11390  elpq  12188  reltre  12548  rpltrp  12549  reltxrnmnf  12550  modmuladd  13095  modmuladdnn0  13097  modfzo0difsn  13125  ssnn0fi  13167  fsuppmapnn0fiubex  13174  wrdl1exs1  13775  cshimadifsn0  14053  reusq0  14682  divconjdvds  15524  2tp1odd  15560  dfgcd2  15749  fissn0dvds  15818  ncoprmlnprm  15923  dvdsprmpweq  16075  oddprmdvds  16094  prmgaplem2  16241  prmgaplcmlem2  16243  prmgaplem5  16246  prmgapprmolem  16252  fullestrcsetc  17272  equivestrcsetc  17273  fullsetcestrc  17287  isnsgrp  17769  mgmnsgrpex  17900  sgrpnmndex  17901  dfgrp2  17929  grplrinv  17957  grpidinv  17959  dfgrp3  17998  ringid  19060  cply1coe0bi  20187  scmatid  20843  scmataddcl  20845  scmatsubcl  20846  scmatmulcl  20847  scmatrhmcl  20857  mat0scmat  20867  symgmatr01lem  20982  cpmatacl  21044  cpmatinvcl  21045  m2cpmfo  21084  pmatcollpw3fi1lem2  21115  gausslemma2dlem1a  25659  2lgslem1b  25686  addsq2reu  25734  addsqrexnreu  25736  addsq2nreurex  25738  2sqreulem1  25740  2sqreunnlem1  25743  islnoppd  26244  outpasch  26259  hlpasch  26260  colopp  26273  colhp  26274  isinagd  26344  inaghl  26350  isleagd  26353  f1otrg  26376  usgredg4  26718  nbupgr  26845  nbumgrvtx  26847  nbgr2vtx1edg  26851  nbuhgr2vtx1edgb  26853  nbusgredgeu  26867  cusgrexilem2  26943  wlkvtxiedg  27125  wlkresOLD  27174  elwwlks2ons3  27477  umgr2cwwkdifex  27605  1pthon2ve  27699  numclwwlk1lem2fo  27916  numclwwlk1lem2foOLD  27921  1stpreimas  30218  cshwrnid  30395  cyc3genpmlem  30497  cyc3genpm  30498  gsummpt2d  30557  fedgmul  30689  ccfldextdgrr  30719  esum2d  31029  reprsuc  31567  reprpmtf1o  31578  fmlasuc  32229  fmla1  32230  unblimceq0lem  33398  unblimceq0  33399  unbdqndv2  33403  knoppndvlem19  33422  3rspcedvd  38581  nnn1suc  38628  prjspertr  38696  prjsperref  38697  prjspersym  38698  prjspvs  38701  0prjspnrel  38710  clsk3nimkb  39787  clsk1indlem1  39792  ntrclsiso  39814  ntrclsk2  39815  ntrclskb  39816  ntrclsk3  39817  ntrclsk13  39818  ntrclsk4  39819  imo72b2lem0  39914  imo72b2lem2  39916  imo72b2lem1  39920  imo72b2  39924  rr-rspce  39957  mnuprdlem4  40020  mnuunid  40022  mnurndlem2  40027  2reu8i  42748  iccelpart  42995  fargshiftfo  43004  sprsymrelf1lem  43051  sprsymrelfo  43057  prproropf1o  43067  paireqne  43071  fmtnoodd  43093  fmtnoprmfac2lem1  43126  fmtnofac2lem  43128  fmtnofac2  43129  fmtnofac1  43130  41prothprm  43182  requad01  43184  dfodd6  43200  dfeven4  43201  opoeALTV  43246  opeoALTV  43247  nn0onn0exALTV  43262  nn0enn0exALTV  43263  nnennexALTV  43264  mogoldbblem  43283  sbgoldbst  43341  sgoldbeven3prm  43346  sbgoldbo  43350  nnsum3primesgbe  43355  nnsum4primesodd  43359  nnsum4primesoddALTV  43360  evengpop3  43361  evengpoap3  43362  nnsum4primeseven  43363  nnsum4primesevenALTV  43364  wtgoldbnnsum4prm  43365  bgoldbnnsum3prm  43367  bgoldbtbndlem4  43371  bgoldbtbnd  43372  bgoldbachlt  43376  tgoldbachlt  43379  isomuspgrlem2d  43394  uspgrsprfo  43421  1odd  43476  nnsgrpnmnd  43483  0even  43596  2even  43598  2zlidl  43599  2zrngamgm  43604  2zrngamnd  43606  2zrngagrp  43608  2zrngmmgm  43611  2zrngnmlid  43614  ply1mulgsumlem1  43837  ply1mulgsumlem2  43838  el0ldep  43918  mod0mul  43977  nn0onn0ex  43981  nn0enn0ex  43982  nnennex  43983  nnpw2p  44044  eenglngeehlnmlem1  44122  eenglngeehlnmlem2  44123  rrx2vlinest  44126  itsclquadb  44161