Theorem rspcedvd 3509

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2156  ∃wrex 3097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-v 3393

This theorem is referenced by:  rspcedeq1vd  3511  rspcedeq2vd  3512  clel5  3538  elpr2elpr  4591  prproe  4628  fsnex  6762  updjud  9043  negfi  11256  fiminre  11257  reltre  12388  rpltrp  12389  reltxrnmnf  12390  modmuladd  12936  modmuladdnn0  12938  modfzo0difsn  12966  ssnn0fi  13008  fsuppmapnn0fiubex  13015  cshimadifsn0  13800  divconjdvds  15260  2tp1odd  15296  dfgcd2  15482  fissn0dvds  15551  ncoprmlnprm  15653  dvdsprmpweq  15805  oddprmdvds  15824  prmgaplem2  15971  prmgaplcmlem2  15973  prmgaplem5  15976  prmgapprmolem  15982  fullestrcsetc  16996  equivestrcsetc  16997  fullsetcestrc  17011  isnsgrp  17493  mgmnsgrpex  17623  sgrpnmndex  17624  dfgrp2  17652  grplrinv  17678  grpidinv  17680  dfgrp3  17719  ringid  18776  cply1coe0bi  19878  scmatid  20531  scmataddcl  20533  scmatsubcl  20534  scmatmulcl  20535  scmatrhmcl  20545  mat0scmat  20555  symgmatr01lem  20671  cpmatacl  20734  cpmatinvcl  20735  m2cpmfo  20774  pmatcollpw3fi1lem2  20805  gausslemma2dlem1a  25304  2lgslem1b  25331  islnoppd  25846  outpasch  25861  hlpasch  25862  colopp  25875  colhp  25876  inaghl  25945  f1otrg  25965  usgredg4  26324  nbupgr  26456  nbumgrvtx  26458  nbgr2vtx1edg  26462  nbuhgr2vtx1edgb  26464  nbusgredgeu  26483  cusgrexilem2  26566  wlkvtxiedg  26748  wlkres  26795  elwwlks2ons3  27095  elwwlks2ons3OLD  27096  umgr2cwwkdifex  27216  1pthon2ve  27327  numclwwlk1lem2fo  27537  1stpreimas  29810  gsummpt2d  30106  esum2d  30480  reprsuc  31018  reprpmtf1o  31029  unblimceq0lem  32814  unblimceq0  32815  unbdqndv2  32819  knoppndvlem19  32838  clsk3nimkb  38838  clsk1indlem1  38843  ntrclsiso  38865  ntrclsk2  38866  ntrclskb  38867  ntrclsk3  38868  ntrclsk13  38869  ntrclsk4  38870  imo72b2lem0  38965  imo72b2lem2  38967  imo72b2lem1  38971  imo72b2  38975  iccelpart  41944  fargshiftfo  41953  fmtnoodd  42020  fmtnoprmfac2lem1  42053  fmtnofac2lem  42055  fmtnofac2  42056  fmtnofac1  42057  41prothprm  42111  dfodd6  42125  dfeven4  42126  opoeALTV  42169  opeoALTV  42170  nn0onn0exALTV  42184  nn0enn0exALTV  42185  mogoldbblem  42204  sbgoldbst  42241  sgoldbeven3prm  42246  sbgoldbo  42250  nnsum3primesgbe  42255  nnsum4primesodd  42259  nnsum4primesoddALTV  42260  evengpop3  42261  evengpoap3  42262  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  wtgoldbnnsum4prm  42265  bgoldbnnsum3prm  42267  bgoldbtbndlem4  42271  bgoldbtbnd  42272  bgoldbachlt  42276  tgoldbachlt  42279  sprsymrelf1lem  42309  sprsymrelfo  42315  uspgrsprfo  42324  1odd  42379  nnsgrpnmnd  42386  0even  42499  2even  42501  2zlidl  42502  2zrngamgm  42507  2zrngamnd  42509  2zrngagrp  42511  2zrngmmgm  42514  2zrngnmlid  42517  ply1mulgsumlem1  42742  ply1mulgsumlem2  42743  el0ldep  42823  mod0mul  42882  nn0onn0ex  42886  nn0enn0ex  42887  nnpw2p  42948