Theorem rspcedvd 3576

Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 3567. (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 3567	. 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  3579  rspcedeq1vd  3581  rspcedeq2vd  3582  fsnex  7211  updjud  9818  modfzo0difsn  13838  ssnn0fi  13880  fsuppmapnn0fiubex  13887  tpfo  14395  wrdl1exs1  14508  cshimadifsn0  14724  reusq0  15359  divconjdvds  16213  2tp1odd  16250  dfgcd2  16444  fissn0dvds  16517  ncoprmlnprm  16626  dvdsprmpweq  16783  oddprmdvds  16802  prmgaplem2  16949  prmgaplcmlem2  16951  prmgaplem5  16954  prmgapprmolem  16960  fullestrcsetc  18044  equivestrcsetc  18045  fullsetcestrc  18059  isnsgrp  18584  efmndmnd  18750  smndex1mnd  18771  smndex1n0mnd  18773  mgmnsgrpex  18792  sgrpnmndex  18793  dfgrp2  18828  grplrinv  18862  grpidinv  18864  dfgrp3  18905  cycsubmcl  19067  cycsubm  19068  ghmquskerlem1  19149  ringid  20146  ringadd2  20148  ringunitnzdiv  20270  rngisomring  20339  rngqiprngimfo  21192  ring2idlqus  21200  pzriprnglem10  21381  pzriprnglem11  21382  cply1coe0bi  22171  evls1maprnss  22247  scmatid  22383  scmataddcl  22385  scmatsubcl  22386  scmatmulcl  22387  scmatrhmcl  22397  mat0scmat  22407  symgmatr01lem  22522  cpmatacl  22585  cpmatinvcl  22586  m2cpmfo  22625  pmatcollpw3fi1lem2  22656  gausslemma2dlem1a  27257  2lgslem1b  27284  addsq2reu  27332  addsqrexnreu  27334  addsq2nreurex  27336  2sqreulem1  27338  2sqreunnlem1  27341  islnoppd  28672  outpasch  28687  hlpasch  28688  colopp  28701  colhp  28702  isinagd  28771  inaghl  28777  isleagd  28780  f1otrg  28803  usgredg4  29149  nbupgr  29276  nbumgrvtx  29278  nbgr2vtx1edg  29282  nbuhgr2vtx1edgb  29284  nbusgredgeu  29298  cusgrexilem2  29374  wlkvtxiedg  29557  elwwlks2ons3  29887  umgr2cwwkdifex  29996  1pthon2ve  30085  numclwwlk1lem2fo  30289  2ndimaxp  32580  1stpreimas  32639  swrdrn3  32892  cshwrnid  32898  gsummpt2d  32997  gsumhashmul  33009  cyc3genpmlem  33088  cyc3genpm  33089  cycpmconjs  33093  cyc3conja  33094  elrgspnlem1  33177  elrgspnsubrunlem2  33183  erlbrd  33198  erler  33200  rloccring  33205  fldgenval  33246  dvdsruassoi  33317  dvdsruasso  33318  lsmsnidl  33332  grplsmid  33337  quslsm  33338  nsgmgc  33345  nsgqusf1olem1  33346  nsgqusf1olem2  33347  nsgqusf1olem3  33348  elrspunidl  33361  elrspunsn  33362  mxidlprm  33403  mxidlirredi  33404  qsdrngilem  33427  1arithidom  33470  fedgmul  33612  ccfldextdgrr  33653  fldextrspunlsplem  33654  irngss  33668  irngnzply1lem  33671  constrsslem  33722  constrconj  33726  constrfiss  33732  constrllcllem  33733  constrlccllem  33734  constrcccllem  33735  nn0constr  33742  ist0cld  33814  zarclsun  33851  zarclsint  33853  zarcmplem  33862  rhmpreimacn  33866  esum2d  34074  reprsuc  34596  reprpmtf1o  34607  fmlasuc  35376  fmla1  35377  satffunlem1lem2  35393  satffunlem2lem2  35396  sategoelfvb  35409  2goelgoanfmla1  35414  unblimceq0lem  36497  unblimceq0  36498  unbdqndv2  36502  knoppndvlem19  36521  aks4d1  42079  primrootsunit1  42087  primrootscoprmpow  42089  primrootscoprbij  42092  remexz  42094  aks6d1c2p2  42109  hashscontpow1  42111  aks6d1c6isolem1  42164  aks6d1c6lem5  42167  unitscyglem5  42189  aks5lem8  42191  3rspcedvd  42205  oacl2g  43320  omcl2  43323  ofoaf  43345  dfno2  43418  clsk3nimkb  44030  clsk1indlem1  44035  ntrclsiso  44057  ntrclsk2  44058  ntrclskb  44059  ntrclsk3  44060  ntrclsk13  44061  ntrclsk4  44062  imo72b2lem0  44155  imo72b2lem2  44157  imo72b2lem1  44159  imo72b2  44162  mnuprdlem4  44265  mnuunid  44267  mnurndlem2  44272  restsubel  45147  fsupdm  46837  finfdm  46841  fsetsniunop  47047  fsetsnf  47049  cfsetsnfsetf  47056  cfsetsnfsetfo  47058  2reu8i  47111  mod0mul  47354  preimafvelsetpreimafv  47386  imasetpreimafvbijlemfo  47403  iccelpart  47431  fargshiftfo  47440  sprsymrelf1lem  47489  sprsymrelfo  47495  prproropf1o  47505  paireqne  47509  fmtnoodd  47531  fmtnoprmfac2lem1  47564  fmtnofac2lem  47566  fmtnofac2  47567  fmtnofac1  47568  41prothprm  47617  requad01  47619  dfodd6  47635  dfeven4  47636  opoeALTV  47681  opeoALTV  47682  nn0onn0exALTV  47697  nn0enn0exALTV  47698  nnennexALTV  47699  mogoldbblem  47718  sbgoldbst  47776  sgoldbeven3prm  47781  sbgoldbo  47785  nnsum3primesgbe  47790  nnsum4primesodd  47794  nnsum4primesoddALTV  47795  evengpop3  47796  evengpoap3  47797  nnsum4primeseven  47798  nnsum4primesevenALTV  47799  wtgoldbnnsum4prm  47800  bgoldbnnsum3prm  47802  bgoldbtbndlem4  47806  bgoldbtbnd  47807  bgoldbachlt  47811  tgoldbachlt  47814  predgclnbgrel  47837  clnbgredg  47838  clnbgrgrimlem  47931  grlimgredgex  47998  gpgprismgriedgdmss  48050  gpgedgvtx0  48059  gpgedgiov  48063  gpg3kgrtriexlem6  48086  gpg3kgrtriex  48087  uspgrsprfo  48146  1odd  48169  nnsgrpnmnd  48176  0even  48235  2even  48237  2zlidl  48238  2zrngamgm  48243  2zrngamnd  48245  2zrngagrp  48247  2zrngmmgm  48250  2zrngnmlid  48253  ply1mulgsumlem1  48385  ply1mulgsumlem2  48386  el0ldep  48465  nn0onn0ex  48522  nn0enn0ex  48523  nnennex  48524  nnpw2p  48585  1arymaptfo  48642  2arymaptfo  48653  eenglngeehlnmlem1  48736  eenglngeehlnmlem2  48737  rrx2vlinest  48740  itsclquadb  48775  iunlub  48819  iinglb  48820