Theorem rspcedvd 3578

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087

This theorem is used by:  rspcime  3581  fsnex  7291  updjud  10018  modfzo0difsn  14089  ssnn0fi  14131  fsuppmapnn0fiubex  14138  tpfo  14648  wrdl1exs1  14765  swrdrn3  14806  cshimadifsn0  14985  reusq0  15637  divconjdvds  16490  2tp1odd  16527  dfgcd2  16724  fissn0dvds  16799  ncoprmlnprm  16909  dvdsprmpweq  17067  oddprmdvds  17086  prmgaplem2  17233  prmgaplcmlem2  17235  prmgaplem5  17238  prmgapprmolem  17244  fullestrcsetc  18330  equivestrcsetc  18331  fullsetcestrc  18345  isnsgrp  18917  efmndmnd  19090  smndex1mnd  19114  smndex1n0mnd  19116  mgmnsgrpex  19135  sgrpnmndex  19136  dfgrp2  19178  grplrinv  19212  grpidinv  19214  dfgrp3  19254  cycsubmcl  19421  cycsubm  19422  ghmquskerlem1  19502  ringid  20508  ringadd2  20510  ringunitnzdiv  20633  rngisomring  20702  rngqiprngimfo  21602  ring2idlqus  21610  pzriprnglem10  21801  pzriprnglem11  21802  cply1coe0bi  22625  evls1maprnss  22701  scmatid  22834  scmataddcl  22836  scmatsubcl  22837  scmatmulcl  22838  scmatrhmcl  22848  mat0scmat  22858  symgmatr01lem  22973  cpmatacl  23039  cpmatinvcl  23040  m2cpmfo  23079  pmatcollpw3fi1lem2  23110  gausslemma2dlem1a  27697  2lgslem1b  27724  addsq2reu  27772  addsqrexnreu  27774  addsq2nreurex  27776  2sqreulem1  27778  2sqreunnlem1  27781  islnoppd  29221  outpasch  29238  hlpasch  29239  colopp  29252  colhp  29253  isinagd  29363  inaghl  29369  isleagd  29372  f1otrg  29453  usgredg4  29803  nbupgr  29930  nbumgrvtx  29932  nbgr2vtx1edg  29936  nbuhgr2vtx1edgb  29938  nbusgredgeu  29952  cusgrexilem2  30028  wlkvtxiedg  30210  elwwlks2ons3  30549  umgr2cwwkdifex  30661  1pthon2ve  30760  numclwwlk1lem2fo  30964  inagcgrasubhl  33054  inagcgratrgw  33060  2ndimaxp  33287  1stpreimas  33346  cshwrnid  33568  gsummpt2d  33656  gsumhashmul  33674  cyc3genpmlem  33758  cyc3genpm  33759  cycpmconjs  33763  cyc3conja  33764  elrgspnlem1  33849  elrgspnsubrunlem2  33855  erlbrd  33870  erler  33872  rloccring  33878  rlocisunit  33883  fldgenval  33920  dvdsruassoi  33985  dvdsruasso  33986  lsmsnidl  33998  grplsmid  34001  quslsm  34002  nsgmgc  34009  nsgqusf1olem1  34010  nsgqusf1olem2  34011  nsgqusf1olem3  34012  elrspunsn  34025  mxidlprm  34041  qsdrngilem  34064  1arithidom  34115  fedgmul  34309  ccfldextdgrr  34350  fldextrspunlsplem  34351  irngss  34365  irngnzply1lem  34368  constrsslem  34419  constrconj  34423  constrfiss  34429  constrllcllem  34430  constrlccllem  34431  constrcccllem  34432  nn0constr  34439  ist0cld  34511  zarclsun  34548  zarclsint  34550  zarcmplem  34559  rhmpreimacn  34563  esum2d  34771  reprsuc  35290  reprpmtf1o  35301  fmlasuc  36237  fmla1  36238  satffunlem1lem2  36254  satffunlem2lem2  36257  sategoelfvb  36270  2goelgoanfmla1  36275  unblimceq0lem  37464  unblimceq0  37465  unbdqndv2  37469  knoppndvlem19  37488  aks4d1  43232  primrootsunit1  43240  primrootscoprmpow  43242  primrootscoprbij  43245  remexz  43247  aks6d1c2p2  43262  hashscontpow1  43264  aks6d1c6isolem1  43317  aks6d1c6lem5  43320  unitscyglem5  43342  aks5lem8  43344  3rspcedvd  43363  oacl2g  44425  omcl2  44428  ofoaf  44450  dfno2  44522  clsk3nimkb  45133  clsk1indlem1  45138  ntrclsiso  45160  ntrclsk2  45161  ntrclskb  45162  ntrclsk3  45163  ntrclsk13  45164  ntrclsk4  45165  imo72b2lem0  45258  imo72b2lem2  45260  imo72b2lem1  45262  imo72b2  45265  mnuprdlem4  45352  mnuunid  45354  mnurndlem2  45359  restsubel  46261  fsupdm  47945  finfdm  47949  fsetsniunop  48212  fsetsnf  48214  cfsetsnfsetf  48221  cfsetsnfsetfo  48223  2reu8i  48276  mod0mul  48525  nndivides2  48547  preimafvelsetpreimafv  48563  imasetpreimafvbijlemfo  48580  iccelpart  48608  fargshiftfo  48617  sprsymrelf1lem  48666  sprsymrelfo  48672  prproropf1o  48682  paireqne  48686  nprmmul3  48704  fmtnoodd  48711  fmtnoprmfac2lem1  48744  fmtnofac2lem  48746  fmtnofac2  48747  fmtnofac1  48748  41prothprm  48797  requad01  48812  dfodd6  48828  dfeven4  48829  opoeALTV  48874  opeoALTV  48875  nn0onn0exALTV  48890  nn0enn0exALTV  48891  nnennexALTV  48892  mogoldbblem  48911  sbgoldbst  48969  sgoldbeven3prm  48974  sbgoldbo  48978  nnsum3primesgbe  48983  nnsum4primesodd  48987  nnsum4primesoddALTV  48988  evengpop3  48989  evengpoap3  48990  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  wtgoldbnnsum4prm  48993  bgoldbnnsum3prm  48995  bgoldbtbndlem4  48999  bgoldbtbnd  49000  bgoldbachlt  49004  tgoldbachlt  49007  predgclnbgrel  49030  clnbgredg  49031  clnbgrgrimlem  49124  grlimgredgex  49191  gpgprismgriedgdmss  49243  gpgedgvtx0  49252  gpgedgiov  49256  gpg3kgrtriexlem6  49279  gpg3kgrtriex  49280  uspgrsprfo  49339  1odd  49361  nnsgrpnmnd  49368  0even  49427  2even  49429  2zlidl  49430  2zrngamgm  49435  2zrngamnd  49437  2zrngagrp  49439  2zrngmmgm  49442  2zrngnmlid  49445  ply1mulgsumlem1  49591  ply1mulgsumlem2  49592  el0ldep  49671  nn0onn0ex  49728  nn0enn0ex  49729  nnennex  49730  nnpw2p  49791  1arymaptfo  49848  2arymaptfo  49859  eenglngeehlnmlem1  49943  eenglngeehlnmlem2  49944  itsclquadb  49981  iunlub  50025  iinglb  50026