Theorem rspcedvd 3637

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077

This theorem is referenced by:  rspcime  3640  rspcedeq1vd  3642  rspcedeq2vd  3643  fsnex  7319  updjud  10003  modfzo0difsn  13994  ssnn0fi  14036  fsuppmapnn0fiubex  14043  tpfo  14549  wrdl1exs1  14661  cshimadifsn0  14879  reusq0  15511  divconjdvds  16363  2tp1odd  16400  dfgcd2  16593  fissn0dvds  16666  ncoprmlnprm  16775  dvdsprmpweq  16931  oddprmdvds  16950  prmgaplem2  17097  prmgaplcmlem2  17099  prmgaplem5  17102  prmgapprmolem  17108  fullestrcsetc  18220  equivestrcsetc  18221  fullsetcestrc  18235  isnsgrp  18761  efmndmnd  18924  smndex1mnd  18945  smndex1n0mnd  18947  mgmnsgrpex  18966  sgrpnmndex  18967  dfgrp2  19002  grplrinv  19036  grpidinv  19038  dfgrp3  19079  cycsubmcl  19241  cycsubm  19242  ghmquskerlem1  19323  ringid  20297  ringadd2  20299  ringunitnzdiv  20424  rngisomring  20493  rngqiprngimfo  21334  ring2idlqus  21342  pzriprnglem10  21524  pzriprnglem11  21525  cply1coe0bi  22327  evls1maprnss  22403  scmatid  22541  scmataddcl  22543  scmatsubcl  22544  scmatmulcl  22545  scmatrhmcl  22555  mat0scmat  22565  symgmatr01lem  22680  cpmatacl  22743  cpmatinvcl  22744  m2cpmfo  22783  pmatcollpw3fi1lem2  22814  gausslemma2dlem1a  27427  2lgslem1b  27454  addsq2reu  27502  addsqrexnreu  27504  addsq2nreurex  27506  2sqreulem1  27508  2sqreunnlem1  27511  islnoppd  28766  outpasch  28781  hlpasch  28782  colopp  28795  colhp  28796  isinagd  28865  inaghl  28871  isleagd  28874  f1otrg  28897  usgredg4  29252  nbupgr  29379  nbumgrvtx  29381  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  nbusgredgeu  29401  cusgrexilem2  29477  wlkvtxiedg  29661  elwwlks2ons3  29988  umgr2cwwkdifex  30097  1pthon2ve  30186  numclwwlk1lem2fo  30390  2ndimaxp  32665  1stpreimas  32717  swrdrn3  32922  cshwrnid  32928  gsummpt2d  33032  gsumhashmul  33040  cyc3genpmlem  33144  cyc3genpm  33145  cycpmconjs  33149  cyc3conja  33150  erlbrd  33235  erler  33237  rloccring  33242  fldgenval  33279  dvdsruassoi  33377  dvdsruasso  33378  lsmsnidl  33392  grplsmid  33397  quslsm  33398  nsgmgc  33405  nsgqusf1olem1  33406  nsgqusf1olem2  33407  nsgqusf1olem3  33408  elrspunidl  33421  elrspunsn  33422  mxidlprm  33463  mxidlirredi  33464  qsdrngilem  33487  1arithidom  33530  fedgmul  33644  ccfldextdgrr  33682  irngss  33687  irngnzply1lem  33690  constrsslem  33731  constrconj  33735  ist0cld  33779  zarclsun  33816  zarclsint  33818  zarcmplem  33827  rhmpreimacn  33831  esum2d  34057  reprsuc  34592  reprpmtf1o  34603  fmlasuc  35354  fmla1  35355  satffunlem1lem2  35371  satffunlem2lem2  35374  sategoelfvb  35387  2goelgoanfmla1  35392  unblimceq0lem  36472  unblimceq0  36473  unbdqndv2  36477  knoppndvlem19  36496  aks4d1  42046  primrootsunit1  42054  primrootscoprmpow  42056  primrootscoprbij  42059  remexz  42061  aks6d1c2p2  42076  hashscontpow1  42078  aks6d1c6isolem1  42131  aks6d1c6lem5  42134  unitscyglem5  42156  aks5lem8  42158  3rspcedvd  42208  oacl2g  43292  omcl2  43295  ofoaf  43317  dfno2  43390  clsk3nimkb  44002  clsk1indlem1  44007  ntrclsiso  44029  ntrclsk2  44030  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  ntrclsk4  44034  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2lem1  44131  imo72b2  44134  mnuprdlem4  44244  mnuunid  44246  mnurndlem2  44251  restsubel  45058  fsupdm  46763  finfdm  46767  fsetsniunop  46964  fsetsnf  46966  cfsetsnfsetf  46973  cfsetsnfsetfo  46975  2reu8i  47028  preimafvelsetpreimafv  47262  imasetpreimafvbijlemfo  47279  iccelpart  47307  fargshiftfo  47316  sprsymrelf1lem  47365  sprsymrelfo  47371  prproropf1o  47381  paireqne  47385  fmtnoodd  47407  fmtnoprmfac2lem1  47440  fmtnofac2lem  47442  fmtnofac2  47443  fmtnofac1  47444  41prothprm  47493  requad01  47495  dfodd6  47511  dfeven4  47512  opoeALTV  47557  opeoALTV  47558  nn0onn0exALTV  47573  nn0enn0exALTV  47574  nnennexALTV  47575  mogoldbblem  47594  sbgoldbst  47652  sgoldbeven3prm  47657  sbgoldbo  47661  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  evengpop3  47672  evengpoap3  47673  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbndlem4  47682  bgoldbtbnd  47683  bgoldbachlt  47687  tgoldbachlt  47690  predgclnbgrel  47711  clnbgredg  47712  clnbgrgrimlem  47785  uspgrsprfo  47871  1odd  47894  nnsgrpnmnd  47901  0even  47960  2even  47962  2zlidl  47963  2zrngamgm  47968  2zrngamnd  47970  2zrngagrp  47972  2zrngmmgm  47975  2zrngnmlid  47978  ply1mulgsumlem1  48115  ply1mulgsumlem2  48116  el0ldep  48195  mod0mul  48253  nn0onn0ex  48257  nn0enn0ex  48258  nnennex  48259  nnpw2p  48320  1arymaptfo  48377  2arymaptfo  48388  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrx2vlinest  48475  itsclquadb  48510