Theorem rspcedvd 3614

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071

This theorem is referenced by:  rspcime  3616  rspcedeq1vd  3618  rspcedeq2vd  3619  elpr2elpr  4869  prproe  4906  fsnex  7283  fsetfocdm  8857  updjud  9931  negfi  12165  elpq  12961  reltre  13321  rpltrp  13322  reltxrnmnf  13323  modmuladd  13880  modmuladdnn0  13882  modfzo0difsn  13910  ssnn0fi  13952  fsuppmapnn0fiubex  13959  wrdl1exs1  14565  cshimadifsn0  14783  reusq0  15411  divconjdvds  16260  2tp1odd  16297  dfgcd2  16490  fissn0dvds  16558  ncoprmlnprm  16666  dvdsprmpweq  16819  oddprmdvds  16838  prmgaplem2  16985  prmgaplcmlem2  16987  prmgaplem5  16990  prmgapprmolem  16996  fullestrcsetc  18105  equivestrcsetc  18106  fullsetcestrc  18120  isnsgrp  18616  efmndmnd  18772  smndex1mnd  18793  smndex1n0mnd  18795  mgmnsgrpex  18814  sgrpnmndex  18815  dfgrp2  18849  grplrinv  18883  grpidinv  18885  dfgrp3  18924  cycsubmcl  19080  cycsubm  19081  ringid  20093  ringadd2  20095  ringunitnzdiv  20216  cply1coe0bi  21831  scmatid  22023  scmataddcl  22025  scmatsubcl  22026  scmatmulcl  22027  scmatrhmcl  22037  mat0scmat  22047  symgmatr01lem  22162  cpmatacl  22225  cpmatinvcl  22226  m2cpmfo  22265  pmatcollpw3fi1lem2  22296  gausslemma2dlem1a  26875  2lgslem1b  26902  addsq2reu  26950  addsqrexnreu  26952  addsq2nreurex  26954  2sqreulem1  26956  2sqreunnlem1  26959  islnoppd  28029  outpasch  28044  hlpasch  28045  colopp  28058  colhp  28059  isinagd  28128  inaghl  28134  isleagd  28137  f1otrg  28160  usgredg4  28512  nbupgr  28639  nbumgrvtx  28641  nbgr2vtx1edg  28645  nbuhgr2vtx1edgb  28647  nbusgredgeu  28661  cusgrexilem2  28737  wlkvtxiedg  28920  elwwlks2ons3  29247  umgr2cwwkdifex  29356  1pthon2ve  29445  numclwwlk1lem2fo  29649  2ndimaxp  31910  1stpreimas  31965  swrdrn3  32157  cshwrnid  32163  gsummpt2d  32242  gsumhashmul  32249  cyc3genpmlem  32351  cyc3genpm  32352  cycpmconjs  32356  cyc3conja  32357  fldgenval  32443  dvdsruassoi  32534  dvdsruasso  32535  lsmsnidl  32554  grplsmid  32559  quslsm  32561  nsgmgc  32568  nsgqusf1olem1  32569  nsgqusf1olem2  32570  nsgqusf1olem3  32571  ghmquskerlem1  32573  elrspunidl  32591  elrspunsn  32592  mxidlprm  32631  mxidlirredi  32632  qsdrngilem  32653  ply1degltdimlem  32766  fedgmul  32775  ccfldextdgrr  32806  irngss  32811  irngnzply1lem  32814  evls1maprnss  32821  ist0cld  32882  zarclsun  32919  zarclsint  32921  zarcmplem  32930  rhmpreimacn  32934  esum2d  33160  reprsuc  33696  reprpmtf1o  33707  fmlasuc  34446  fmla1  34447  satffunlem1lem2  34463  satffunlem2lem2  34466  sategoelfvb  34479  2goelgoanfmla1  34484  unblimceq0lem  35468  unblimceq0  35469  unbdqndv2  35473  knoppndvlem19  35492  aks4d1  41040  aks6d1c2p2  41043  3rspcedvd  41117  fsuppind  41244  nnn1suc  41262  sn-negex12  41371  prjspertr  41429  prjsperref  41430  prjspersym  41431  prjspvs  41434  0prjspnrel  41451  oacl2g  42162  omcl2  42165  ofoaf  42187  dfno2  42261  clsk3nimkb  42873  clsk1indlem1  42878  ntrclsiso  42900  ntrclsk2  42901  ntrclskb  42902  ntrclsk3  42903  ntrclsk13  42904  ntrclsk4  42905  imo72b2lem0  42999  imo72b2lem2  43001  imo72b2lem1  43003  imo72b2  43006  mnuprdlem4  43116  mnuunid  43118  mnurndlem2  43123  restsubel  43929  fsupdm  45637  finfdm  45641  fsetsniunop  45838  fsetsnf  45840  cfsetsnfsetf  45847  cfsetsnfsetfo  45849  2reu8i  45900  preimafvelsetpreimafv  46135  imasetpreimafvbijlemfo  46152  iccelpart  46180  fargshiftfo  46189  sprsymrelf1lem  46238  sprsymrelfo  46244  prproropf1o  46254  paireqne  46258  fmtnoodd  46280  fmtnoprmfac2lem1  46313  fmtnofac2lem  46315  fmtnofac2  46316  fmtnofac1  46317  41prothprm  46366  requad01  46368  dfodd6  46384  dfeven4  46385  opoeALTV  46430  opeoALTV  46431  nn0onn0exALTV  46446  nn0enn0exALTV  46447  nnennexALTV  46448  mogoldbblem  46467  sbgoldbst  46525  sgoldbeven3prm  46530  sbgoldbo  46534  nnsum3primesgbe  46539  nnsum4primesodd  46543  nnsum4primesoddALTV  46544  evengpop3  46545  evengpoap3  46546  nnsum4primeseven  46547  nnsum4primesevenALTV  46548  wtgoldbnnsum4prm  46549  bgoldbnnsum3prm  46551  bgoldbtbndlem4  46555  bgoldbtbnd  46556  bgoldbachlt  46560  tgoldbachlt  46563  isomuspgrlem2d  46578  uspgrsprfo  46605  1odd  46660  nnsgrpnmnd  46667  rngisomring  46798  rngqiprngimfo  46865  ring2idlqus  46873  pzriprnglem10  46893  pzriprnglem11  46894  0even  46908  2even  46910  2zlidl  46911  2zrngamgm  46916  2zrngamnd  46918  2zrngagrp  46920  2zrngmmgm  46923  2zrngnmlid  46926  ply1mulgsumlem1  47145  ply1mulgsumlem2  47146  el0ldep  47225  mod0mul  47283  nn0onn0ex  47287  nn0enn0ex  47288  nnennex  47289  nnpw2p  47350  1arymaptfo  47407  2arymaptfo  47418  eenglngeehlnmlem1  47501  eenglngeehlnmlem2  47502  rrx2vlinest  47505  itsclquadb  47540