Theorem rspcedvd 3575

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3057

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058

This theorem is referenced by:  rspcime  3578  rspcedeq1vd  3580  rspcedeq2vd  3581  fsnex  7223  updjud  9834  modfzo0difsn  13852  ssnn0fi  13894  fsuppmapnn0fiubex  13901  tpfo  14409  wrdl1exs1  14523  cshimadifsn0  14739  reusq0  15374  divconjdvds  16228  2tp1odd  16265  dfgcd2  16459  fissn0dvds  16532  ncoprmlnprm  16641  dvdsprmpweq  16798  oddprmdvds  16817  prmgaplem2  16964  prmgaplcmlem2  16966  prmgaplem5  16969  prmgapprmolem  16975  fullestrcsetc  18059  equivestrcsetc  18060  fullsetcestrc  18074  isnsgrp  18633  efmndmnd  18799  smndex1mnd  18820  smndex1n0mnd  18822  mgmnsgrpex  18841  sgrpnmndex  18842  dfgrp2  18877  grplrinv  18911  grpidinv  18913  dfgrp3  18954  cycsubmcl  19115  cycsubm  19116  ghmquskerlem1  19197  ringid  20194  ringadd2  20196  ringunitnzdiv  20318  rngisomring  20387  rngqiprngimfo  21240  ring2idlqus  21248  pzriprnglem10  21429  pzriprnglem11  21430  cply1coe0bi  22218  evls1maprnss  22294  scmatid  22430  scmataddcl  22432  scmatsubcl  22433  scmatmulcl  22434  scmatrhmcl  22444  mat0scmat  22454  symgmatr01lem  22569  cpmatacl  22632  cpmatinvcl  22633  m2cpmfo  22672  pmatcollpw3fi1lem2  22703  gausslemma2dlem1a  27304  2lgslem1b  27331  addsq2reu  27379  addsqrexnreu  27381  addsq2nreurex  27383  2sqreulem1  27385  2sqreunnlem1  27388  islnoppd  28719  outpasch  28734  hlpasch  28735  colopp  28748  colhp  28749  isinagd  28818  inaghl  28824  isleagd  28827  f1otrg  28850  usgredg4  29197  nbupgr  29324  nbumgrvtx  29326  nbgr2vtx1edg  29330  nbuhgr2vtx1edgb  29332  nbusgredgeu  29346  cusgrexilem2  29422  wlkvtxiedg  29605  elwwlks2ons3  29935  umgr2cwwkdifex  30047  1pthon2ve  30136  numclwwlk1lem2fo  30340  2ndimaxp  32630  1stpreimas  32691  swrdrn3  32943  cshwrnid  32949  gsummpt2d  33036  gsumhashmul  33048  cyc3genpmlem  33127  cyc3genpm  33128  cycpmconjs  33132  cyc3conja  33133  elrgspnlem1  33216  elrgspnsubrunlem2  33222  erlbrd  33237  erler  33239  rloccring  33244  fldgenval  33285  dvdsruassoi  33356  dvdsruasso  33357  lsmsnidl  33371  grplsmid  33376  quslsm  33377  nsgmgc  33384  nsgqusf1olem1  33385  nsgqusf1olem2  33386  nsgqusf1olem3  33387  elrspunidl  33400  elrspunsn  33401  mxidlprm  33442  mxidlirredi  33443  qsdrngilem  33466  1arithidom  33509  fedgmul  33665  ccfldextdgrr  33706  fldextrspunlsplem  33707  irngss  33721  irngnzply1lem  33724  constrsslem  33775  constrconj  33779  constrfiss  33785  constrllcllem  33786  constrlccllem  33787  constrcccllem  33788  nn0constr  33795  ist0cld  33867  zarclsun  33904  zarclsint  33906  zarcmplem  33915  rhmpreimacn  33919  esum2d  34127  reprsuc  34649  reprpmtf1o  34660  fmlasuc  35451  fmla1  35452  satffunlem1lem2  35468  satffunlem2lem2  35471  sategoelfvb  35484  2goelgoanfmla1  35489  unblimceq0lem  36571  unblimceq0  36572  unbdqndv2  36576  knoppndvlem19  36595  aks4d1  42202  primrootsunit1  42210  primrootscoprmpow  42212  primrootscoprbij  42215  remexz  42217  aks6d1c2p2  42232  hashscontpow1  42234  aks6d1c6isolem1  42287  aks6d1c6lem5  42290  unitscyglem5  42312  aks5lem8  42314  3rspcedvd  42333  oacl2g  43447  omcl2  43450  ofoaf  43472  dfno2  43545  clsk3nimkb  44157  clsk1indlem1  44162  ntrclsiso  44184  ntrclsk2  44185  ntrclskb  44186  ntrclsk3  44187  ntrclsk13  44188  ntrclsk4  44189  imo72b2lem0  44282  imo72b2lem2  44284  imo72b2lem1  44286  imo72b2  44289  mnuprdlem4  44392  mnuunid  44394  mnurndlem2  44399  restsubel  45274  fsupdm  46964  finfdm  46968  fsetsniunop  47173  fsetsnf  47175  cfsetsnfsetf  47182  cfsetsnfsetfo  47184  2reu8i  47237  mod0mul  47480  preimafvelsetpreimafv  47512  imasetpreimafvbijlemfo  47529  iccelpart  47557  fargshiftfo  47566  sprsymrelf1lem  47615  sprsymrelfo  47621  prproropf1o  47631  paireqne  47635  fmtnoodd  47657  fmtnoprmfac2lem1  47690  fmtnofac2lem  47692  fmtnofac2  47693  fmtnofac1  47694  41prothprm  47743  requad01  47745  dfodd6  47761  dfeven4  47762  opoeALTV  47807  opeoALTV  47808  nn0onn0exALTV  47823  nn0enn0exALTV  47824  nnennexALTV  47825  mogoldbblem  47844  sbgoldbst  47902  sgoldbeven3prm  47907  sbgoldbo  47911  nnsum3primesgbe  47916  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  evengpop3  47922  evengpoap3  47923  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  wtgoldbnnsum4prm  47926  bgoldbnnsum3prm  47928  bgoldbtbndlem4  47932  bgoldbtbnd  47933  bgoldbachlt  47937  tgoldbachlt  47940  predgclnbgrel  47963  clnbgredg  47964  clnbgrgrimlem  48057  grlimgredgex  48124  gpgprismgriedgdmss  48176  gpgedgvtx0  48185  gpgedgiov  48189  gpg3kgrtriexlem6  48212  gpg3kgrtriex  48213  uspgrsprfo  48272  1odd  48295  nnsgrpnmnd  48302  0even  48361  2even  48363  2zlidl  48364  2zrngamgm  48369  2zrngamnd  48371  2zrngagrp  48373  2zrngmmgm  48376  2zrngnmlid  48379  ply1mulgsumlem1  48511  ply1mulgsumlem2  48512  el0ldep  48591  nn0onn0ex  48648  nn0enn0ex  48649  nnennex  48650  nnpw2p  48711  1arymaptfo  48768  2arymaptfo  48779  eenglngeehlnmlem1  48862  eenglngeehlnmlem2  48863  rrx2vlinest  48866  itsclquadb  48901  iunlub  48945  iinglb  48946