Theorem rspcedvd 3626

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144

This theorem is referenced by:  rspcime  3627  rspcedeq1vd  3629  rspcedeq2vd  3630  clel5OLD  3658  elpr2elpr  4799  prproe  4836  fsnex  7039  updjud  9363  negfi  11589  fiminreOLD  11590  elpq  12375  reltre  12734  rpltrp  12735  reltxrnmnf  12736  modmuladd  13282  modmuladdnn0  13284  modfzo0difsn  13312  ssnn0fi  13354  fsuppmapnn0fiubex  13361  wrdl1exs1  13967  cshimadifsn0  14192  reusq0  14822  divconjdvds  15665  2tp1odd  15701  dfgcd2  15894  fissn0dvds  15963  ncoprmlnprm  16068  dvdsprmpweq  16220  oddprmdvds  16239  prmgaplem2  16386  prmgaplcmlem2  16388  prmgaplem5  16391  prmgapprmolem  16397  fullestrcsetc  17401  equivestrcsetc  17402  fullsetcestrc  17416  isnsgrp  17905  efmndmnd  18054  smndex1mnd  18075  smndex1n0mnd  18077  mgmnsgrpex  18096  sgrpnmndex  18097  dfgrp2  18128  grplrinv  18157  grpidinv  18159  dfgrp3  18198  cycsubmcl  18344  cycsubm  18345  ringid  19324  cply1coe0bi  20468  scmatid  21123  scmataddcl  21125  scmatsubcl  21126  scmatmulcl  21127  scmatrhmcl  21137  mat0scmat  21147  symgmatr01lem  21262  cpmatacl  21324  cpmatinvcl  21325  m2cpmfo  21364  pmatcollpw3fi1lem2  21395  gausslemma2dlem1a  25941  2lgslem1b  25968  addsq2reu  26016  addsqrexnreu  26018  addsq2nreurex  26020  2sqreulem1  26022  2sqreunnlem1  26025  islnoppd  26526  outpasch  26541  hlpasch  26542  colopp  26555  colhp  26556  isinagd  26625  inaghl  26631  isleagd  26634  f1otrg  26657  usgredg4  26999  nbupgr  27126  nbumgrvtx  27128  nbgr2vtx1edg  27132  nbuhgr2vtx1edgb  27134  nbusgredgeu  27148  cusgrexilem2  27224  wlkvtxiedg  27406  elwwlks2ons3  27734  umgr2cwwkdifex  27844  1pthon2ve  27933  numclwwlk1lem2fo  28137  1stpreimas  30441  swrdrn3  30629  cshwrnid  30635  gsummpt2d  30687  cyc3genpmlem  30793  cyc3genpm  30794  cycpmconjs  30798  cyc3conja  30799  lsmsnidl  30949  mxidlprm  30977  fedgmul  31027  ccfldextdgrr  31057  esum2d  31352  reprsuc  31886  reprpmtf1o  31897  fmlasuc  32633  fmla1  32634  satffunlem1lem2  32650  satffunlem2lem2  32653  sategoelfvb  32666  2goelgoanfmla1  32671  unblimceq0lem  33845  unblimceq0  33846  unbdqndv2  33850  knoppndvlem19  33869  3rspcedvd  39125  nnn1suc  39179  prjspertr  39275  prjsperref  39276  prjspersym  39277  prjspvs  39280  0prjspnrel  39289  clsk3nimkb  40410  clsk1indlem1  40415  ntrclsiso  40437  ntrclsk2  40438  ntrclskb  40439  ntrclsk3  40440  ntrclsk13  40441  ntrclsk4  40442  imo72b2lem0  40536  imo72b2lem2  40538  imo72b2lem1  40541  imo72b2  40545  mnuprdlem4  40631  mnuunid  40633  mnurndlem2  40638  2reu8i  43332  preimafvelsetpreimafv  43568  imasetpreimafvbijlemfo  43585  iccelpart  43613  fargshiftfo  43622  sprsymrelf1lem  43673  sprsymrelfo  43679  prproropf1o  43689  paireqne  43693  fmtnoodd  43715  fmtnoprmfac2lem1  43748  fmtnofac2lem  43750  fmtnofac2  43751  fmtnofac1  43752  41prothprm  43804  requad01  43806  dfodd6  43822  dfeven4  43823  opoeALTV  43868  opeoALTV  43869  nn0onn0exALTV  43884  nn0enn0exALTV  43885  nnennexALTV  43886  mogoldbblem  43905  sbgoldbst  43963  sgoldbeven3prm  43968  sbgoldbo  43972  nnsum3primesgbe  43977  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  evengpop3  43983  evengpoap3  43984  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  wtgoldbnnsum4prm  43987  bgoldbnnsum3prm  43989  bgoldbtbndlem4  43993  bgoldbtbnd  43994  bgoldbachlt  43998  tgoldbachlt  44001  isomuspgrlem2d  44016  uspgrsprfo  44043  1odd  44098  nnsgrpnmnd  44105  0even  44222  2even  44224  2zlidl  44225  2zrngamgm  44230  2zrngamnd  44232  2zrngagrp  44234  2zrngmmgm  44237  2zrngnmlid  44240  ply1mulgsumlem1  44460  ply1mulgsumlem2  44461  el0ldep  44541  mod0mul  44599  nn0onn0ex  44603  nn0enn0ex  44604  nnennex  44605  nnpw2p  44666  eenglngeehlnmlem1  44744  eenglngeehlnmlem2  44745  rrx2vlinest  44748  itsclquadb  44783