Theorem rspcedvd 3555

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069

This theorem is referenced by:  rspcime  3556  rspcedeq1vd  3558  rspcedeq2vd  3559  elpr2elpr  4796  prproe  4834  fsnex  7135  fsetfocdm  8607  updjud  9623  negfi  11854  elpq  12644  reltre  13003  rpltrp  13004  reltxrnmnf  13005  modmuladd  13561  modmuladdnn0  13563  modfzo0difsn  13591  ssnn0fi  13633  fsuppmapnn0fiubex  13640  wrdl1exs1  14246  cshimadifsn0  14471  reusq0  15102  divconjdvds  15952  2tp1odd  15989  dfgcd2  16182  fissn0dvds  16252  ncoprmlnprm  16360  dvdsprmpweq  16513  oddprmdvds  16532  prmgaplem2  16679  prmgaplcmlem2  16681  prmgaplem5  16684  prmgapprmolem  16690  fullestrcsetc  17784  equivestrcsetc  17785  fullsetcestrc  17799  isnsgrp  18294  efmndmnd  18443  smndex1mnd  18464  smndex1n0mnd  18466  mgmnsgrpex  18485  sgrpnmndex  18486  dfgrp2  18519  grplrinv  18548  grpidinv  18550  dfgrp3  18589  cycsubmcl  18735  cycsubm  18736  ringid  19728  cply1coe0bi  21381  scmatid  21571  scmataddcl  21573  scmatsubcl  21574  scmatmulcl  21575  scmatrhmcl  21585  mat0scmat  21595  symgmatr01lem  21710  cpmatacl  21773  cpmatinvcl  21774  m2cpmfo  21813  pmatcollpw3fi1lem2  21844  gausslemma2dlem1a  26418  2lgslem1b  26445  addsq2reu  26493  addsqrexnreu  26495  addsq2nreurex  26497  2sqreulem1  26499  2sqreunnlem1  26502  islnoppd  27005  outpasch  27020  hlpasch  27021  colopp  27034  colhp  27035  isinagd  27104  inaghl  27110  isleagd  27113  f1otrg  27136  usgredg4  27487  nbupgr  27614  nbumgrvtx  27616  nbgr2vtx1edg  27620  nbuhgr2vtx1edgb  27622  nbusgredgeu  27636  cusgrexilem2  27712  wlkvtxiedg  27894  elwwlks2ons3  28221  umgr2cwwkdifex  28330  1pthon2ve  28419  numclwwlk1lem2fo  28623  2ndimaxp  30885  1stpreimas  30940  swrdrn3  31129  cshwrnid  31135  gsummpt2d  31211  gsumhashmul  31218  cyc3genpmlem  31320  cyc3genpm  31321  cycpmconjs  31325  cyc3conja  31326  lsmsnidl  31489  grplsmid  31494  quslsm  31495  nsgmgc  31499  nsgqusf1olem1  31500  nsgqusf1olem2  31501  nsgqusf1olem3  31502  elrspunidl  31508  mxidlprm  31542  fedgmul  31614  ccfldextdgrr  31644  ist0cld  31685  zarclsun  31722  zarclsint  31724  zarcmplem  31733  rhmpreimacn  31737  esum2d  31961  reprsuc  32495  reprpmtf1o  32506  fmlasuc  33248  fmla1  33249  satffunlem1lem2  33265  satffunlem2lem2  33268  sategoelfvb  33281  2goelgoanfmla1  33286  unblimceq0lem  34613  unblimceq0  34614  unbdqndv2  34618  knoppndvlem19  34637  aks4d1  40025  3rspcedvd  40110  fsuppind  40202  nnn1suc  40217  sn-negex12  40319  prjspertr  40365  prjsperref  40366  prjspersym  40367  prjspvs  40370  0prjspnrel  40385  clsk3nimkb  41539  clsk1indlem1  41544  ntrclsiso  41566  ntrclsk2  41567  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  ntrclsk4  41571  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2lem1  41669  imo72b2  41672  mnuprdlem4  41782  mnuunid  41784  mnurndlem2  41789  fsetsniunop  44430  fsetsnf  44432  cfsetsnfsetf  44439  cfsetsnfsetfo  44441  2reu8i  44492  preimafvelsetpreimafv  44728  imasetpreimafvbijlemfo  44745  iccelpart  44773  fargshiftfo  44782  sprsymrelf1lem  44831  sprsymrelfo  44837  prproropf1o  44847  paireqne  44851  fmtnoodd  44873  fmtnoprmfac2lem1  44906  fmtnofac2lem  44908  fmtnofac2  44909  fmtnofac1  44910  41prothprm  44959  requad01  44961  dfodd6  44977  dfeven4  44978  opoeALTV  45023  opeoALTV  45024  nn0onn0exALTV  45039  nn0enn0exALTV  45040  nnennexALTV  45041  mogoldbblem  45060  sbgoldbst  45118  sgoldbeven3prm  45123  sbgoldbo  45127  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  evengpop3  45138  evengpoap3  45139  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem4  45148  bgoldbtbnd  45149  bgoldbachlt  45153  tgoldbachlt  45156  isomuspgrlem2d  45171  uspgrsprfo  45198  1odd  45253  nnsgrpnmnd  45260  0even  45377  2even  45379  2zlidl  45380  2zrngamgm  45385  2zrngamnd  45387  2zrngagrp  45389  2zrngmmgm  45392  2zrngnmlid  45395  ply1mulgsumlem1  45615  ply1mulgsumlem2  45616  el0ldep  45695  mod0mul  45753  nn0onn0ex  45757  nn0enn0ex  45758  nnennex  45759  nnpw2p  45820  1arymaptfo  45877  2arymaptfo  45888  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  rrx2vlinest  45975  itsclquadb  46010