Theorem rspcedvd 3593

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055

This theorem is referenced by:  rspcime  3596  rspcedeq1vd  3598  rspcedeq2vd  3599  fsnex  7261  updjud  9894  modfzo0difsn  13915  ssnn0fi  13957  fsuppmapnn0fiubex  13964  tpfo  14472  wrdl1exs1  14585  cshimadifsn0  14803  reusq0  15438  divconjdvds  16292  2tp1odd  16329  dfgcd2  16523  fissn0dvds  16596  ncoprmlnprm  16705  dvdsprmpweq  16862  oddprmdvds  16881  prmgaplem2  17028  prmgaplcmlem2  17030  prmgaplem5  17033  prmgapprmolem  17039  fullestrcsetc  18119  equivestrcsetc  18120  fullsetcestrc  18134  isnsgrp  18657  efmndmnd  18823  smndex1mnd  18844  smndex1n0mnd  18846  mgmnsgrpex  18865  sgrpnmndex  18866  dfgrp2  18901  grplrinv  18935  grpidinv  18937  dfgrp3  18978  cycsubmcl  19140  cycsubm  19141  ghmquskerlem1  19222  ringid  20190  ringadd2  20192  ringunitnzdiv  20314  rngisomring  20383  rngqiprngimfo  21218  ring2idlqus  21226  pzriprnglem10  21407  pzriprnglem11  21408  cply1coe0bi  22196  evls1maprnss  22272  scmatid  22408  scmataddcl  22410  scmatsubcl  22411  scmatmulcl  22412  scmatrhmcl  22422  mat0scmat  22432  symgmatr01lem  22547  cpmatacl  22610  cpmatinvcl  22611  m2cpmfo  22650  pmatcollpw3fi1lem2  22681  gausslemma2dlem1a  27283  2lgslem1b  27310  addsq2reu  27358  addsqrexnreu  27360  addsq2nreurex  27362  2sqreulem1  27364  2sqreunnlem1  27367  islnoppd  28674  outpasch  28689  hlpasch  28690  colopp  28703  colhp  28704  isinagd  28773  inaghl  28779  isleagd  28782  f1otrg  28805  usgredg4  29151  nbupgr  29278  nbumgrvtx  29280  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  nbusgredgeu  29300  cusgrexilem2  29376  wlkvtxiedg  29560  elwwlks2ons3  29892  umgr2cwwkdifex  30001  1pthon2ve  30090  numclwwlk1lem2fo  30294  2ndimaxp  32577  1stpreimas  32636  swrdrn3  32884  cshwrnid  32890  gsummpt2d  32996  gsumhashmul  33008  cyc3genpmlem  33115  cyc3genpm  33116  cycpmconjs  33120  cyc3conja  33121  elrgspnlem1  33200  elrgspnsubrunlem2  33206  erlbrd  33221  erler  33223  rloccring  33228  fldgenval  33269  dvdsruassoi  33362  dvdsruasso  33363  lsmsnidl  33377  grplsmid  33382  quslsm  33383  nsgmgc  33390  nsgqusf1olem1  33391  nsgqusf1olem2  33392  nsgqusf1olem3  33393  elrspunidl  33406  elrspunsn  33407  mxidlprm  33448  mxidlirredi  33449  qsdrngilem  33472  1arithidom  33515  fedgmul  33634  ccfldextdgrr  33674  fldextrspunlsplem  33675  irngss  33689  irngnzply1lem  33692  constrsslem  33738  constrconj  33742  constrfiss  33748  constrllcllem  33749  constrlccllem  33750  constrcccllem  33751  nn0constr  33758  ist0cld  33830  zarclsun  33867  zarclsint  33869  zarcmplem  33878  rhmpreimacn  33882  esum2d  34090  reprsuc  34613  reprpmtf1o  34624  fmlasuc  35380  fmla1  35381  satffunlem1lem2  35397  satffunlem2lem2  35400  sategoelfvb  35413  2goelgoanfmla1  35418  unblimceq0lem  36501  unblimceq0  36502  unbdqndv2  36506  knoppndvlem19  36525  aks4d1  42084  primrootsunit1  42092  primrootscoprmpow  42094  primrootscoprbij  42097  remexz  42099  aks6d1c2p2  42114  hashscontpow1  42116  aks6d1c6isolem1  42169  aks6d1c6lem5  42172  unitscyglem5  42194  aks5lem8  42196  3rspcedvd  42210  oacl2g  43326  omcl2  43329  ofoaf  43351  dfno2  43424  clsk3nimkb  44036  clsk1indlem1  44041  ntrclsiso  44063  ntrclsk2  44064  ntrclskb  44065  ntrclsk3  44066  ntrclsk13  44067  ntrclsk4  44068  imo72b2lem0  44161  imo72b2lem2  44163  imo72b2lem1  44165  imo72b2  44168  mnuprdlem4  44271  mnuunid  44273  mnurndlem2  44278  restsubel  45154  fsupdm  46847  finfdm  46851  fsetsniunop  47054  fsetsnf  47056  cfsetsnfsetf  47063  cfsetsnfsetfo  47065  2reu8i  47118  mod0mul  47361  preimafvelsetpreimafv  47393  imasetpreimafvbijlemfo  47410  iccelpart  47438  fargshiftfo  47447  sprsymrelf1lem  47496  sprsymrelfo  47502  prproropf1o  47512  paireqne  47516  fmtnoodd  47538  fmtnoprmfac2lem1  47571  fmtnofac2lem  47573  fmtnofac2  47574  fmtnofac1  47575  41prothprm  47624  requad01  47626  dfodd6  47642  dfeven4  47643  opoeALTV  47688  opeoALTV  47689  nn0onn0exALTV  47704  nn0enn0exALTV  47705  nnennexALTV  47706  mogoldbblem  47725  sbgoldbst  47783  sgoldbeven3prm  47788  sbgoldbo  47792  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  evengpop3  47803  evengpoap3  47804  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbndlem4  47813  bgoldbtbnd  47814  bgoldbachlt  47818  tgoldbachlt  47821  predgclnbgrel  47843  clnbgredg  47844  clnbgrgrimlem  47937  gpgprismgriedgdmss  48047  gpgedgvtx0  48056  gpgedgiov  48060  gpg3kgrtriexlem6  48083  gpg3kgrtriex  48084  uspgrsprfo  48140  1odd  48163  nnsgrpnmnd  48170  0even  48229  2even  48231  2zlidl  48232  2zrngamgm  48237  2zrngamnd  48239  2zrngagrp  48241  2zrngmmgm  48244  2zrngnmlid  48247  ply1mulgsumlem1  48379  ply1mulgsumlem2  48380  el0ldep  48459  nn0onn0ex  48516  nn0enn0ex  48517  nnennex  48518  nnpw2p  48579  1arymaptfo  48636  2arymaptfo  48647  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  rrx2vlinest  48734  itsclquadb  48769  iunlub  48813  iinglb  48814