Theorem rspcedvd 3603

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061

This theorem is referenced by:  rspcime  3606  rspcedeq1vd  3608  rspcedeq2vd  3609  fsnex  7276  updjud  9948  modfzo0difsn  13961  ssnn0fi  14003  fsuppmapnn0fiubex  14010  tpfo  14518  wrdl1exs1  14631  cshimadifsn0  14849  reusq0  15481  divconjdvds  16334  2tp1odd  16371  dfgcd2  16565  fissn0dvds  16638  ncoprmlnprm  16747  dvdsprmpweq  16904  oddprmdvds  16923  prmgaplem2  17070  prmgaplcmlem2  17072  prmgaplem5  17075  prmgapprmolem  17081  fullestrcsetc  18163  equivestrcsetc  18164  fullsetcestrc  18178  isnsgrp  18701  efmndmnd  18867  smndex1mnd  18888  smndex1n0mnd  18890  mgmnsgrpex  18909  sgrpnmndex  18910  dfgrp2  18945  grplrinv  18979  grpidinv  18981  dfgrp3  19022  cycsubmcl  19184  cycsubm  19185  ghmquskerlem1  19266  ringid  20234  ringadd2  20236  ringunitnzdiv  20358  rngisomring  20427  rngqiprngimfo  21262  ring2idlqus  21270  pzriprnglem10  21451  pzriprnglem11  21452  cply1coe0bi  22240  evls1maprnss  22316  scmatid  22452  scmataddcl  22454  scmatsubcl  22455  scmatmulcl  22456  scmatrhmcl  22466  mat0scmat  22476  symgmatr01lem  22591  cpmatacl  22654  cpmatinvcl  22655  m2cpmfo  22694  pmatcollpw3fi1lem2  22725  gausslemma2dlem1a  27328  2lgslem1b  27355  addsq2reu  27403  addsqrexnreu  27405  addsq2nreurex  27407  2sqreulem1  27409  2sqreunnlem1  27412  islnoppd  28719  outpasch  28734  hlpasch  28735  colopp  28748  colhp  28749  isinagd  28818  inaghl  28824  isleagd  28827  f1otrg  28850  usgredg4  29196  nbupgr  29323  nbumgrvtx  29325  nbgr2vtx1edg  29329  nbuhgr2vtx1edgb  29331  nbusgredgeu  29345  cusgrexilem2  29421  wlkvtxiedg  29605  elwwlks2ons3  29937  umgr2cwwkdifex  30046  1pthon2ve  30135  numclwwlk1lem2fo  30339  2ndimaxp  32624  1stpreimas  32683  swrdrn3  32931  cshwrnid  32937  gsummpt2d  33043  gsumhashmul  33055  cyc3genpmlem  33162  cyc3genpm  33163  cycpmconjs  33167  cyc3conja  33168  elrgspnlem1  33237  elrgspnsubrunlem2  33243  erlbrd  33258  erler  33260  rloccring  33265  fldgenval  33306  dvdsruassoi  33399  dvdsruasso  33400  lsmsnidl  33414  grplsmid  33419  quslsm  33420  nsgmgc  33427  nsgqusf1olem1  33428  nsgqusf1olem2  33429  nsgqusf1olem3  33430  elrspunidl  33443  elrspunsn  33444  mxidlprm  33485  mxidlirredi  33486  qsdrngilem  33509  1arithidom  33552  fedgmul  33671  ccfldextdgrr  33713  fldextrspunlsplem  33714  irngss  33728  irngnzply1lem  33731  constrsslem  33775  constrconj  33779  constrfiss  33785  constrllcllem  33786  constrlccllem  33787  constrcccllem  33788  nn0constr  33795  ist0cld  33864  zarclsun  33901  zarclsint  33903  zarcmplem  33912  rhmpreimacn  33916  esum2d  34124  reprsuc  34647  reprpmtf1o  34658  fmlasuc  35408  fmla1  35409  satffunlem1lem2  35425  satffunlem2lem2  35428  sategoelfvb  35441  2goelgoanfmla1  35446  unblimceq0lem  36524  unblimceq0  36525  unbdqndv2  36529  knoppndvlem19  36548  aks4d1  42102  primrootsunit1  42110  primrootscoprmpow  42112  primrootscoprbij  42115  remexz  42117  aks6d1c2p2  42132  hashscontpow1  42134  aks6d1c6isolem1  42187  aks6d1c6lem5  42190  unitscyglem5  42212  aks5lem8  42214  3rspcedvd  42266  oacl2g  43354  omcl2  43357  ofoaf  43379  dfno2  43452  clsk3nimkb  44064  clsk1indlem1  44069  ntrclsiso  44091  ntrclsk2  44092  ntrclskb  44093  ntrclsk3  44094  ntrclsk13  44095  ntrclsk4  44096  imo72b2lem0  44189  imo72b2lem2  44191  imo72b2lem1  44193  imo72b2  44196  mnuprdlem4  44299  mnuunid  44301  mnurndlem2  44306  restsubel  45177  fsupdm  46871  finfdm  46875  fsetsniunop  47078  fsetsnf  47080  cfsetsnfsetf  47087  cfsetsnfsetfo  47089  2reu8i  47142  preimafvelsetpreimafv  47402  imasetpreimafvbijlemfo  47419  iccelpart  47447  fargshiftfo  47456  sprsymrelf1lem  47505  sprsymrelfo  47511  prproropf1o  47521  paireqne  47525  fmtnoodd  47547  fmtnoprmfac2lem1  47580  fmtnofac2lem  47582  fmtnofac2  47583  fmtnofac1  47584  41prothprm  47633  requad01  47635  dfodd6  47651  dfeven4  47652  opoeALTV  47697  opeoALTV  47698  nn0onn0exALTV  47713  nn0enn0exALTV  47714  nnennexALTV  47715  mogoldbblem  47734  sbgoldbst  47792  sgoldbeven3prm  47797  sbgoldbo  47801  nnsum3primesgbe  47806  nnsum4primesodd  47810  nnsum4primesoddALTV  47811  evengpop3  47812  evengpoap3  47813  nnsum4primeseven  47814  nnsum4primesevenALTV  47815  wtgoldbnnsum4prm  47816  bgoldbnnsum3prm  47818  bgoldbtbndlem4  47822  bgoldbtbnd  47823  bgoldbachlt  47827  tgoldbachlt  47830  predgclnbgrel  47852  clnbgredg  47853  clnbgrgrimlem  47946  gpgprismgriedgdmss  48056  gpgedgvtx0  48065  gpg3kgrtriexlem6  48090  gpg3kgrtriex  48091  uspgrsprfo  48123  1odd  48146  nnsgrpnmnd  48153  0even  48212  2even  48214  2zlidl  48215  2zrngamgm  48220  2zrngamnd  48222  2zrngagrp  48224  2zrngmmgm  48227  2zrngnmlid  48230  ply1mulgsumlem1  48362  ply1mulgsumlem2  48363  el0ldep  48442  mod0mul  48499  nn0onn0ex  48503  nn0enn0ex  48504  nnennex  48505  nnpw2p  48566  1arymaptfo  48623  2arymaptfo  48634  eenglngeehlnmlem1  48717  eenglngeehlnmlem2  48718  rrx2vlinest  48721  itsclquadb  48756  iunlub  48799  iinglb  48800