Theorem rspcedvd 3582

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091

This theorem is used by:  rspcime  3585  fsnex  7314  updjud  10042  modfzo0difsn  14113  ssnn0fi  14155  fsuppmapnn0fiubex  14162  tpfo  14672  wrdl1exs1  14789  swrdrn3  14830  cshimadifsn0  15009  reusq0  15661  divconjdvds  16514  2tp1odd  16551  dfgcd2  16748  fissn0dvds  16823  ncoprmlnprm  16933  dvdsprmpweq  17091  oddprmdvds  17110  prmgaplem2  17257  prmgaplcmlem2  17259  prmgaplem5  17262  prmgapprmolem  17268  fullestrcsetc  18354  equivestrcsetc  18355  fullsetcestrc  18369  isnsgrp  18941  efmndmnd  19114  smndex1mnd  19138  smndex1n0mnd  19140  mgmnsgrpex  19159  sgrpnmndex  19160  dfgrp2  19202  grplrinv  19236  grpidinv  19238  dfgrp3  19278  cycsubmcl  19445  cycsubm  19446  ghmquskerlem1  19527  ringid  20533  ringadd2  20535  ringunitnzdiv  20658  rngisomring  20727  rngqiprngimfo  21627  ring2idlqus  21635  pzriprnglem10  21826  pzriprnglem11  21827  cply1coe0bi  22650  evls1maprnss  22726  scmatid  22859  scmataddcl  22861  scmatsubcl  22862  scmatmulcl  22863  scmatrhmcl  22873  mat0scmat  22883  symgmatr01lem  22998  cpmatacl  23064  cpmatinvcl  23065  m2cpmfo  23104  pmatcollpw3fi1lem2  23135  gausslemma2dlem1a  27722  2lgslem1b  27749  addsq2reu  27797  addsqrexnreu  27799  addsq2nreurex  27801  2sqreulem1  27803  2sqreunnlem1  27806  islnoppd  29246  outpasch  29263  hlpasch  29264  colopp  29277  colhp  29278  isinagd  29388  inaghl  29394  isleagd  29397  f1otrg  29478  usgredg4  29828  nbupgr  29955  nbumgrvtx  29957  nbgr2vtx1edg  29961  nbuhgr2vtx1edgb  29963  nbusgredgeu  29977  cusgrexilem2  30053  wlkvtxiedg  30235  elwwlks2ons3  30574  umgr2cwwkdifex  30686  1pthon2ve  30785  numclwwlk1lem2fo  30989  inagcgrasubhl  33079  inagcgratrgw  33085  2ndimaxp  33312  1stpreimas  33370  cshwrnid  33592  gsummpt2d  33680  gsumhashmul  33698  cyc3genpmlem  33782  cyc3genpm  33783  cycpmconjs  33787  cyc3conja  33788  elrgspnlem1  33873  elrgspnsubrunlem2  33879  erlbrd  33894  erler  33896  rloccring  33902  rlocisunit  33907  fldgenval  33944  dvdsruassoi  34009  dvdsruasso  34010  lsmsnidl  34022  grplsmid  34025  quslsm  34026  nsgmgc  34033  nsgqusf1olem1  34034  nsgqusf1olem2  34035  nsgqusf1olem3  34036  elrspunsn  34049  mxidlprm  34065  qsdrngilem  34088  1arithidom  34139  fedgmul  34333  ccfldextdgrr  34374  fldextrspunlsplem  34375  irngss  34389  irngnzply1lem  34392  constrsslem  34443  constrconj  34447  constrfiss  34453  constrllcllem  34454  constrlccllem  34455  constrcccllem  34456  nn0constr  34463  ist0cld  34535  zarclsun  34572  zarclsint  34574  zarcmplem  34583  rhmpreimacn  34587  esum2d  34795  reprsuc  35314  reprpmtf1o  35325  fmlasuc  36318  fmla1  36319  satffunlem1lem2  36335  satffunlem2lem2  36338  sategoelfvb  36351  2goelgoanfmla1  36356  unblimceq0lem  37550  unblimceq0  37551  unbdqndv2  37555  knoppndvlem19  37574  aks4d1  43331  primrootsunit1  43339  primrootscoprmpow  43341  primrootscoprbij  43344  remexz  43346  aks6d1c2p2  43361  hashscontpow1  43363  aks6d1c6isolem1  43416  aks6d1c6lem5  43419  unitscyglem5  43441  aks5lem8  43443  3rspcedvd  43463  oacl2g  44524  omcl2  44527  ofoaf  44549  dfno2  44621  clsk3nimkb  45232  clsk1indlem1  45237  ntrclsiso  45259  ntrclsk2  45260  ntrclskb  45261  ntrclsk3  45262  ntrclsk13  45263  ntrclsk4  45264  imo72b2lem0  45357  imo72b2lem2  45359  imo72b2lem1  45361  imo72b2  45364  mnuprdlem4  45451  mnuunid  45453  mnurndlem2  45458  restsubel  46373  fsupdm  48057  finfdm  48061  fsetsniunop  48324  fsetsnf  48326  cfsetsnfsetf  48333  cfsetsnfsetfo  48335  2reu8i  48389  mod0mul  48637  nndivides2  48659  preimafvelsetpreimafv  48675  imasetpreimafvbijlemfo  48692  iccelpart  48720  fargshiftfo  48729  sprsymrelf1lem  48778  sprsymrelfo  48784  prproropf1o  48794  paireqne  48798  nprmmul3  48816  fmtnoodd  48823  fmtnoprmfac2lem1  48856  fmtnofac2lem  48858  fmtnofac2  48859  fmtnofac1  48860  41prothprm  48909  requad01  48924  dfodd6  48940  dfeven4  48941  opoeALTV  48986  opeoALTV  48987  nn0onn0exALTV  49002  nn0enn0exALTV  49003  nnennexALTV  49004  mogoldbblem  49023  sbgoldbst  49081  sgoldbeven3prm  49086  sbgoldbo  49090  nnsum3primesgbe  49095  nnsum4primesodd  49099  nnsum4primesoddALTV  49100  evengpop3  49101  evengpoap3  49102  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  wtgoldbnnsum4prm  49105  bgoldbnnsum3prm  49107  bgoldbtbndlem4  49111  bgoldbtbnd  49112  bgoldbachlt  49116  tgoldbachlt  49119  predgclnbgrel  49142  clnbgredg  49143  clnbgrgrimlem  49236  grlimgredgex  49303  gpgprismgriedgdmss  49355  gpgedgvtx0  49364  gpgedgiov  49368  gpg3kgrtriexlem6  49391  gpg3kgrtriex  49392  uspgrsprfo  49451  1odd  49473  nnsgrpnmnd  49480  0even  49539  2even  49541  2zlidl  49542  2zrngamgm  49547  2zrngamnd  49549  2zrngagrp  49551  2zrngmmgm  49554  2zrngnmlid  49557  ply1mulgsumlem1  49703  ply1mulgsumlem2  49704  el0ldep  49783  nn0onn0ex  49840  nn0enn0ex  49841  nnennex  49842  nnpw2p  49903  1arymaptfo  49960  2arymaptfo  49971  eenglngeehlnmlem1  50055  eenglngeehlnmlem2  50056  itsclquadb  50093  iunlub  50137  iinglb  50138