Theorem rspcedvd 3563

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066

This theorem is referenced by:  rspcime  3566  fsnex  7230  updjud  9853  modfzo0difsn  13900  ssnn0fi  13942  fsuppmapnn0fiubex  13949  tpfo  14457  wrdl1exs1  14571  cshimadifsn0  14787  reusq0  15422  divconjdvds  16279  2tp1odd  16316  dfgcd2  16510  fissn0dvds  16583  ncoprmlnprm  16693  dvdsprmpweq  16850  oddprmdvds  16869  prmgaplem2  17016  prmgaplcmlem2  17018  prmgaplem5  17021  prmgapprmolem  17027  fullestrcsetc  18112  equivestrcsetc  18113  fullsetcestrc  18127  isnsgrp  18686  efmndmnd  18852  smndex1mnd  18876  smndex1n0mnd  18878  mgmnsgrpex  18897  sgrpnmndex  18898  dfgrp2  18933  grplrinv  18967  grpidinv  18969  dfgrp3  19010  cycsubmcl  19171  cycsubm  19172  ghmquskerlem1  19252  ringid  20249  ringadd2  20251  ringunitnzdiv  20372  rngisomring  20441  rngqiprngimfo  21297  ring2idlqus  21305  pzriprnglem10  21468  pzriprnglem11  21469  cply1coe0bi  22291  evls1maprnss  22367  scmatid  22500  scmataddcl  22502  scmatsubcl  22503  scmatmulcl  22504  scmatrhmcl  22514  mat0scmat  22524  symgmatr01lem  22639  cpmatacl  22702  cpmatinvcl  22703  m2cpmfo  22742  pmatcollpw3fi1lem2  22773  gausslemma2dlem1a  27349  2lgslem1b  27376  addsq2reu  27424  addsqrexnreu  27426  addsq2nreurex  27428  2sqreulem1  27430  2sqreunnlem1  27433  islnoppd  28828  outpasch  28843  hlpasch  28844  colopp  28857  colhp  28858  isinagd  28927  inaghl  28933  isleagd  28936  f1otrg  28959  usgredg4  29306  nbupgr  29433  nbumgrvtx  29435  nbgr2vtx1edg  29439  nbuhgr2vtx1edgb  29441  nbusgredgeu  29455  cusgrexilem2  29531  wlkvtxiedg  29713  elwwlks2ons3  30043  umgr2cwwkdifex  30155  1pthon2ve  30244  numclwwlk1lem2fo  30448  2ndimaxp  32740  1stpreimas  32800  swrdrn3  33036  cshwrnid  33042  gsummpt2d  33132  gsumhashmul  33150  cyc3genpmlem  33234  cyc3genpm  33235  cycpmconjs  33239  cyc3conja  33240  elrgspnlem1  33325  elrgspnsubrunlem2  33331  erlbrd  33346  erler  33348  rloccring  33353  fldgenval  33398  dvdsruassoi  33469  dvdsruasso  33470  lsmsnidl  33484  grplsmid  33489  quslsm  33490  nsgmgc  33497  nsgqusf1olem1  33498  nsgqusf1olem2  33499  nsgqusf1olem3  33500  elrspunidl  33513  elrspunsn  33514  mxidlprm  33555  qsdrngilem  33579  1arithidom  33630  fedgmul  33825  ccfldextdgrr  33866  fldextrspunlsplem  33867  irngss  33881  irngnzply1lem  33884  constrsslem  33935  constrconj  33939  constrfiss  33945  constrllcllem  33946  constrlccllem  33947  constrcccllem  33948  nn0constr  33955  ist0cld  34027  zarclsun  34064  zarclsint  34066  zarcmplem  34075  rhmpreimacn  34079  esum2d  34287  reprsuc  34809  reprpmtf1o  34820  fmlasuc  35627  fmla1  35628  satffunlem1lem2  35644  satffunlem2lem2  35647  sategoelfvb  35660  2goelgoanfmla1  35665  unblimceq0lem  36825  unblimceq0  36826  unbdqndv2  36830  knoppndvlem19  36849  aks4d1  42587  primrootsunit1  42595  primrootscoprmpow  42597  primrootscoprbij  42600  remexz  42602  aks6d1c2p2  42617  hashscontpow1  42619  aks6d1c6isolem1  42672  aks6d1c6lem5  42675  unitscyglem5  42697  aks5lem8  42699  3rspcedvd  42716  oacl2g  43788  omcl2  43791  ofoaf  43813  dfno2  43885  clsk3nimkb  44497  clsk1indlem1  44502  ntrclsiso  44524  ntrclsk2  44525  ntrclskb  44526  ntrclsk3  44527  ntrclsk13  44528  ntrclsk4  44529  imo72b2lem0  44622  imo72b2lem2  44624  imo72b2lem1  44626  imo72b2  44629  mnuprdlem4  44732  mnuunid  44734  mnurndlem2  44739  restsubel  45612  fsupdm  47297  finfdm  47301  fsetsniunop  47524  fsetsnf  47526  cfsetsnfsetf  47533  cfsetsnfsetfo  47535  2reu8i  47588  mod0mul  47837  nndivides2  47859  preimafvelsetpreimafv  47875  imasetpreimafvbijlemfo  47892  iccelpart  47920  fargshiftfo  47929  sprsymrelf1lem  47978  sprsymrelfo  47984  prproropf1o  47994  paireqne  47998  nprmmul3  48016  fmtnoodd  48023  fmtnoprmfac2lem1  48056  fmtnofac2lem  48058  fmtnofac2  48059  fmtnofac1  48060  41prothprm  48109  requad01  48124  dfodd6  48140  dfeven4  48141  opoeALTV  48186  opeoALTV  48187  nn0onn0exALTV  48202  nn0enn0exALTV  48203  nnennexALTV  48204  mogoldbblem  48223  sbgoldbst  48281  sgoldbeven3prm  48286  sbgoldbo  48290  nnsum3primesgbe  48295  nnsum4primesodd  48299  nnsum4primesoddALTV  48300  evengpop3  48301  evengpoap3  48302  nnsum4primeseven  48303  nnsum4primesevenALTV  48304  wtgoldbnnsum4prm  48305  bgoldbnnsum3prm  48307  bgoldbtbndlem4  48311  bgoldbtbnd  48312  bgoldbachlt  48316  tgoldbachlt  48319  predgclnbgrel  48342  clnbgredg  48343  clnbgrgrimlem  48436  grlimgredgex  48503  gpgprismgriedgdmss  48555  gpgedgvtx0  48564  gpgedgiov  48568  gpg3kgrtriexlem6  48591  gpg3kgrtriex  48592  uspgrsprfo  48651  1odd  48674  nnsgrpnmnd  48681  0even  48740  2even  48742  2zlidl  48743  2zrngamgm  48748  2zrngamnd  48750  2zrngagrp  48752  2zrngmmgm  48755  2zrngnmlid  48758  ply1mulgsumlem1  48889  ply1mulgsumlem2  48890  el0ldep  48969  nn0onn0ex  49026  nn0enn0ex  49027  nnennex  49028  nnpw2p  49089  1arymaptfo  49146  2arymaptfo  49157  eenglngeehlnmlem1  49240  eenglngeehlnmlem2  49241  rrx2vlinest  49244  itsclquadb  49279  iunlub  49323  iinglb  49324