Theorem rspcedvd 3289

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175

This theorem is referenced by:  rspcedeq1vd  3290  rspcedeq2vd  3291  elpr2elpr  4336  fsnex  6438  negfi  10850  fiminre  10851  reltre  12041  rpltrp  12042  reltxrnmnf  12043  modmuladd  12574  modmuladdnn0  12576  modfzo0difsn  12604  ssnn0fi  12646  fsuppmapnn0fiubex  12654  cshimadifsn0  13427  divconjdvds  14875  2tp1odd  14914  dfgcd2  15101  fissn0dvds  15170  ncoprmlnprm  15274  dvdsprmpweq  15426  oddprmdvds  15445  prmgaplem2  15592  prmgaplcmlem2  15594  prmgaplem5  15597  prmgapprmolem  15603  fullestrcsetc  16614  equivestrcsetc  16615  fullsetcestrc  16629  isnsgrp  17111  mgmnsgrpex  17241  sgrpnmndex  17242  dfgrp2  17270  grplrinv  17296  grpidinv  17298  dfgrp3  17337  ringid  18397  cply1coe0bi  19491  scmatid  20139  scmataddcl  20141  scmatsubcl  20142  scmatmulcl  20143  scmatrhmcl  20153  mat0scmat  20163  symgmatr01lem  20278  cpmatacl  20340  cpmatinvcl  20341  m2cpmfo  20380  pmatcollpw3fi1lem2  20411  gausslemma2dlem1a  24890  2lgslem1b  24917  islnoppd  25432  outpasch  25447  hlpasch  25448  colopp  25461  colhp  25462  inaghl  25531  f1otrg  25551  fargshiftfo  26166  usg2cwwkdifex  26349  numclwlk1lem2fo  26622  1stpreimas  28866  gsummpt2d  29112  esum2d  29482  unblimceq0lem  31667  unblimceq0  31668  unbdqndv2  31672  knoppndvlem19  31691  clsk3nimkb  37358  clsk1indlem1  37363  ntrclsiso  37385  ntrclsk2  37386  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  ntrclsk4  37390  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  iccelpart  39971  fmtnoodd  39983  fmtnoprmfac2lem1  40016  fmtnofac2lem  40018  fmtnofac2  40019  fmtnofac1  40020  41prothprm  40074  dfodd6  40088  dfeven4  40089  opoeALTV  40132  opeoALTV  40133  nn0onn0exALTV  40147  nn0enn0exALTV  40148  bgoldbst  40200  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  evengpop3  40214  evengpoap3  40215  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbndlem4  40224  bgoldbtbnd  40225  bgoldbachlt  40227  tgoldbachlt  40230  bgoldbachltOLD  40234  tgoldbachltOLD  40237  clel5  40303  usgredg4  40444  nbupgr  40566  nbumgrvtx  40568  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  nbusgredgeu  40594  cusgrexi  40662  1wlkvtxiedg  40829  1wlkres  40879  elwwlks2ons3  41159  umgr2cwwkdifex  41249  1pthon2ve  41321  av-numclwlk1lem2fo  41525  1odd  41601  nnsgrpnmnd  41608  0even  41721  2even  41723  2zlidl  41724  2zrngamgm  41729  2zrngamnd  41731  2zrngagrp  41733  2zrngmmgm  41736  2zrngnmlid  41739  ply1mulgsumlem1  41968  ply1mulgsumlem2  41969  el0ldep  42049  mod0mul  42108  nn0onn0ex  42112  nn0enn0ex  42113  nnpw2p  42178