Theorem rspcedvd 3590

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  rspcime  3593  rspcedeq1vd  3595  rspcedeq2vd  3596  fsnex  7258  updjud  9887  modfzo0difsn  13908  ssnn0fi  13950  fsuppmapnn0fiubex  13957  tpfo  14465  wrdl1exs1  14578  cshimadifsn0  14796  reusq0  15431  divconjdvds  16285  2tp1odd  16322  dfgcd2  16516  fissn0dvds  16589  ncoprmlnprm  16698  dvdsprmpweq  16855  oddprmdvds  16874  prmgaplem2  17021  prmgaplcmlem2  17023  prmgaplem5  17026  prmgapprmolem  17032  fullestrcsetc  18112  equivestrcsetc  18113  fullsetcestrc  18127  isnsgrp  18650  efmndmnd  18816  smndex1mnd  18837  smndex1n0mnd  18839  mgmnsgrpex  18858  sgrpnmndex  18859  dfgrp2  18894  grplrinv  18928  grpidinv  18930  dfgrp3  18971  cycsubmcl  19133  cycsubm  19134  ghmquskerlem1  19215  ringid  20183  ringadd2  20185  ringunitnzdiv  20307  rngisomring  20376  rngqiprngimfo  21211  ring2idlqus  21219  pzriprnglem10  21400  pzriprnglem11  21401  cply1coe0bi  22189  evls1maprnss  22265  scmatid  22401  scmataddcl  22403  scmatsubcl  22404  scmatmulcl  22405  scmatrhmcl  22415  mat0scmat  22425  symgmatr01lem  22540  cpmatacl  22603  cpmatinvcl  22604  m2cpmfo  22643  pmatcollpw3fi1lem2  22674  gausslemma2dlem1a  27276  2lgslem1b  27303  addsq2reu  27351  addsqrexnreu  27353  addsq2nreurex  27355  2sqreulem1  27357  2sqreunnlem1  27360  islnoppd  28667  outpasch  28682  hlpasch  28683  colopp  28696  colhp  28697  isinagd  28766  inaghl  28772  isleagd  28775  f1otrg  28798  usgredg4  29144  nbupgr  29271  nbumgrvtx  29273  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  nbusgredgeu  29293  cusgrexilem2  29369  wlkvtxiedg  29553  elwwlks2ons3  29885  umgr2cwwkdifex  29994  1pthon2ve  30083  numclwwlk1lem2fo  30287  2ndimaxp  32570  1stpreimas  32629  swrdrn3  32877  cshwrnid  32883  gsummpt2d  32989  gsumhashmul  33001  cyc3genpmlem  33108  cyc3genpm  33109  cycpmconjs  33113  cyc3conja  33114  elrgspnlem1  33193  elrgspnsubrunlem2  33199  erlbrd  33214  erler  33216  rloccring  33221  fldgenval  33262  dvdsruassoi  33355  dvdsruasso  33356  lsmsnidl  33370  grplsmid  33375  quslsm  33376  nsgmgc  33383  nsgqusf1olem1  33384  nsgqusf1olem2  33385  nsgqusf1olem3  33386  elrspunidl  33399  elrspunsn  33400  mxidlprm  33441  mxidlirredi  33442  qsdrngilem  33465  1arithidom  33508  fedgmul  33627  ccfldextdgrr  33667  fldextrspunlsplem  33668  irngss  33682  irngnzply1lem  33685  constrsslem  33731  constrconj  33735  constrfiss  33741  constrllcllem  33742  constrlccllem  33743  constrcccllem  33744  nn0constr  33751  ist0cld  33823  zarclsun  33860  zarclsint  33862  zarcmplem  33871  rhmpreimacn  33875  esum2d  34083  reprsuc  34606  reprpmtf1o  34617  fmlasuc  35373  fmla1  35374  satffunlem1lem2  35390  satffunlem2lem2  35393  sategoelfvb  35406  2goelgoanfmla1  35411  unblimceq0lem  36494  unblimceq0  36495  unbdqndv2  36499  knoppndvlem19  36518  aks4d1  42077  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  remexz  42092  aks6d1c2p2  42107  hashscontpow1  42109  aks6d1c6isolem1  42162  aks6d1c6lem5  42165  unitscyglem5  42187  aks5lem8  42189  3rspcedvd  42203  oacl2g  43319  omcl2  43322  ofoaf  43344  dfno2  43417  clsk3nimkb  44029  clsk1indlem1  44034  ntrclsiso  44056  ntrclsk2  44057  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrclsk4  44061  imo72b2lem0  44154  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  mnuprdlem4  44264  mnuunid  44266  mnurndlem2  44271  restsubel  45147  fsupdm  46840  finfdm  46844  fsetsniunop  47050  fsetsnf  47052  cfsetsnfsetf  47059  cfsetsnfsetfo  47061  2reu8i  47114  mod0mul  47357  preimafvelsetpreimafv  47389  imasetpreimafvbijlemfo  47406  iccelpart  47434  fargshiftfo  47443  sprsymrelf1lem  47492  sprsymrelfo  47498  prproropf1o  47508  paireqne  47512  fmtnoodd  47534  fmtnoprmfac2lem1  47567  fmtnofac2lem  47569  fmtnofac2  47570  fmtnofac1  47571  41prothprm  47620  requad01  47622  dfodd6  47638  dfeven4  47639  opoeALTV  47684  opeoALTV  47685  nn0onn0exALTV  47700  nn0enn0exALTV  47701  nnennexALTV  47702  mogoldbblem  47721  sbgoldbst  47779  sgoldbeven3prm  47784  sbgoldbo  47788  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  evengpop3  47799  evengpoap3  47800  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem4  47809  bgoldbtbnd  47810  bgoldbachlt  47814  tgoldbachlt  47817  predgclnbgrel  47839  clnbgredg  47840  clnbgrgrimlem  47933  gpgprismgriedgdmss  48043  gpgedgvtx0  48052  gpgedgiov  48056  gpg3kgrtriexlem6  48079  gpg3kgrtriex  48080  uspgrsprfo  48136  1odd  48159  nnsgrpnmnd  48166  0even  48225  2even  48227  2zlidl  48228  2zrngamgm  48233  2zrngamnd  48235  2zrngagrp  48237  2zrngmmgm  48240  2zrngnmlid  48243  ply1mulgsumlem1  48375  ply1mulgsumlem2  48376  el0ldep  48455  nn0onn0ex  48512  nn0enn0ex  48513  nnennex  48514  nnpw2p  48575  1arymaptfo  48632  2arymaptfo  48643  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2vlinest  48730  itsclquadb  48765  iunlub  48809  iinglb  48810