Theorem rspcedvd 3574

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃wrex 3107

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112

This theorem is referenced by:  rspcime  3575  rspcedeq1vd  3577  rspcedeq2vd  3578  elpr2elpr  4759  prproe  4798  fsnex  7017  updjud  9347  negfi  11577  elpq  12362  reltre  12721  rpltrp  12722  reltxrnmnf  12723  modmuladd  13276  modmuladdnn0  13278  modfzo0difsn  13306  ssnn0fi  13348  fsuppmapnn0fiubex  13355  wrdl1exs1  13958  cshimadifsn0  14183  reusq0  14814  divconjdvds  15657  2tp1odd  15693  dfgcd2  15884  fissn0dvds  15953  ncoprmlnprm  16058  dvdsprmpweq  16210  oddprmdvds  16229  prmgaplem2  16376  prmgaplcmlem2  16378  prmgaplem5  16381  prmgapprmolem  16387  fullestrcsetc  17393  equivestrcsetc  17394  fullsetcestrc  17408  isnsgrp  17897  efmndmnd  18046  smndex1mnd  18067  smndex1n0mnd  18069  mgmnsgrpex  18088  sgrpnmndex  18089  dfgrp2  18120  grplrinv  18149  grpidinv  18151  dfgrp3  18190  cycsubmcl  18336  cycsubm  18337  ringid  19320  cply1coe0bi  20929  scmatid  21119  scmataddcl  21121  scmatsubcl  21122  scmatmulcl  21123  scmatrhmcl  21133  mat0scmat  21143  symgmatr01lem  21258  cpmatacl  21321  cpmatinvcl  21322  m2cpmfo  21361  pmatcollpw3fi1lem2  21392  gausslemma2dlem1a  25949  2lgslem1b  25976  addsq2reu  26024  addsqrexnreu  26026  addsq2nreurex  26028  2sqreulem1  26030  2sqreunnlem1  26033  islnoppd  26534  outpasch  26549  hlpasch  26550  colopp  26563  colhp  26564  isinagd  26633  inaghl  26639  isleagd  26642  f1otrg  26665  usgredg4  27007  nbupgr  27134  nbumgrvtx  27136  nbgr2vtx1edg  27140  nbuhgr2vtx1edgb  27142  nbusgredgeu  27156  cusgrexilem2  27232  wlkvtxiedg  27414  elwwlks2ons3  27741  umgr2cwwkdifex  27850  1pthon2ve  27939  numclwwlk1lem2fo  28143  2ndimaxp  30409  1stpreimas  30465  swrdrn3  30655  cshwrnid  30661  gsummpt2d  30734  gsumhashmul  30741  cyc3genpmlem  30843  cyc3genpm  30844  cycpmconjs  30848  cyc3conja  30849  lsmsnidl  31006  elrspunidl  31014  mxidlprm  31048  fedgmul  31115  ccfldextdgrr  31145  ist0cld  31186  zarclsun  31223  zarclsint  31225  zarcmplem  31234  rhmpreimacn  31238  esum2d  31462  reprsuc  31996  reprpmtf1o  32007  fmlasuc  32746  fmla1  32747  satffunlem1lem2  32763  satffunlem2lem2  32766  sategoelfvb  32779  2goelgoanfmla1  32784  unblimceq0lem  33958  unblimceq0  33959  unbdqndv2  33963  knoppndvlem19  33982  3rspcedvd  39397  fsuppind  39456  nnn1suc  39467  sn-negex12  39553  prjspertr  39599  prjsperref  39600  prjspersym  39601  prjspvs  39604  0prjspnrel  39613  clsk3nimkb  40743  clsk1indlem1  40748  ntrclsiso  40770  ntrclsk2  40771  ntrclskb  40772  ntrclsk3  40773  ntrclsk13  40774  ntrclsk4  40775  imo72b2lem0  40869  imo72b2lem2  40871  imo72b2lem1  40874  imo72b2  40878  mnuprdlem4  40983  mnuunid  40985  mnurndlem2  40990  2reu8i  43669  preimafvelsetpreimafv  43905  imasetpreimafvbijlemfo  43922  iccelpart  43950  fargshiftfo  43959  sprsymrelf1lem  44008  sprsymrelfo  44014  prproropf1o  44024  paireqne  44028  fmtnoodd  44050  fmtnoprmfac2lem1  44083  fmtnofac2lem  44085  fmtnofac2  44086  fmtnofac1  44087  41prothprm  44137  requad01  44139  dfodd6  44155  dfeven4  44156  opoeALTV  44201  opeoALTV  44202  nn0onn0exALTV  44217  nn0enn0exALTV  44218  nnennexALTV  44219  mogoldbblem  44238  sbgoldbst  44296  sgoldbeven3prm  44301  sbgoldbo  44305  nnsum3primesgbe  44310  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  evengpop3  44316  evengpoap3  44317  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  bgoldbtbndlem4  44326  bgoldbtbnd  44327  bgoldbachlt  44331  tgoldbachlt  44334  isomuspgrlem2d  44349  uspgrsprfo  44376  1odd  44431  nnsgrpnmnd  44438  0even  44555  2even  44557  2zlidl  44558  2zrngamgm  44563  2zrngamnd  44565  2zrngagrp  44567  2zrngmmgm  44570  2zrngnmlid  44573  ply1mulgsumlem1  44794  ply1mulgsumlem2  44795  el0ldep  44875  mod0mul  44933  nn0onn0ex  44937  nn0enn0ex  44938  nnennex  44939  nnpw2p  45000  1arymaptfo  45057  2arymaptfo  45068  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  rrx2vlinest  45155  itsclquadb  45190