Theorem rspcedvd 3581

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  rspcime  3584  rspcedeq1vd  3586  rspcedeq2vd  3587  fsnex  7224  updjud  9849  modfzo0difsn  13868  ssnn0fi  13910  fsuppmapnn0fiubex  13917  tpfo  14425  wrdl1exs1  14538  cshimadifsn0  14755  reusq0  15390  divconjdvds  16244  2tp1odd  16281  dfgcd2  16475  fissn0dvds  16548  ncoprmlnprm  16657  dvdsprmpweq  16814  oddprmdvds  16833  prmgaplem2  16980  prmgaplcmlem2  16982  prmgaplem5  16985  prmgapprmolem  16991  fullestrcsetc  18075  equivestrcsetc  18076  fullsetcestrc  18090  isnsgrp  18615  efmndmnd  18781  smndex1mnd  18802  smndex1n0mnd  18804  mgmnsgrpex  18823  sgrpnmndex  18824  dfgrp2  18859  grplrinv  18893  grpidinv  18895  dfgrp3  18936  cycsubmcl  19098  cycsubm  19099  ghmquskerlem1  19180  ringid  20177  ringadd2  20179  ringunitnzdiv  20301  rngisomring  20370  rngqiprngimfo  21226  ring2idlqus  21234  pzriprnglem10  21415  pzriprnglem11  21416  cply1coe0bi  22205  evls1maprnss  22281  scmatid  22417  scmataddcl  22419  scmatsubcl  22420  scmatmulcl  22421  scmatrhmcl  22431  mat0scmat  22441  symgmatr01lem  22556  cpmatacl  22619  cpmatinvcl  22620  m2cpmfo  22659  pmatcollpw3fi1lem2  22690  gausslemma2dlem1a  27292  2lgslem1b  27319  addsq2reu  27367  addsqrexnreu  27369  addsq2nreurex  27371  2sqreulem1  27373  2sqreunnlem1  27376  islnoppd  28703  outpasch  28718  hlpasch  28719  colopp  28732  colhp  28733  isinagd  28802  inaghl  28808  isleagd  28811  f1otrg  28834  usgredg4  29180  nbupgr  29307  nbumgrvtx  29309  nbgr2vtx1edg  29313  nbuhgr2vtx1edgb  29315  nbusgredgeu  29329  cusgrexilem2  29405  wlkvtxiedg  29588  elwwlks2ons3  29918  umgr2cwwkdifex  30027  1pthon2ve  30116  numclwwlk1lem2fo  30320  2ndimaxp  32603  1stpreimas  32662  swrdrn3  32910  cshwrnid  32916  gsummpt2d  33015  gsumhashmul  33027  cyc3genpmlem  33106  cyc3genpm  33107  cycpmconjs  33111  cyc3conja  33112  elrgspnlem1  33192  elrgspnsubrunlem2  33198  erlbrd  33213  erler  33215  rloccring  33220  fldgenval  33261  dvdsruassoi  33331  dvdsruasso  33332  lsmsnidl  33346  grplsmid  33351  quslsm  33352  nsgmgc  33359  nsgqusf1olem1  33360  nsgqusf1olem2  33361  nsgqusf1olem3  33362  elrspunidl  33375  elrspunsn  33376  mxidlprm  33417  mxidlirredi  33418  qsdrngilem  33441  1arithidom  33484  fedgmul  33603  ccfldextdgrr  33643  fldextrspunlsplem  33644  irngss  33658  irngnzply1lem  33661  constrsslem  33707  constrconj  33711  constrfiss  33717  constrllcllem  33718  constrlccllem  33719  constrcccllem  33720  nn0constr  33727  ist0cld  33799  zarclsun  33836  zarclsint  33838  zarcmplem  33847  rhmpreimacn  33851  esum2d  34059  reprsuc  34582  reprpmtf1o  34593  fmlasuc  35358  fmla1  35359  satffunlem1lem2  35375  satffunlem2lem2  35378  sategoelfvb  35391  2goelgoanfmla1  35396  unblimceq0lem  36479  unblimceq0  36480  unbdqndv2  36484  knoppndvlem19  36503  aks4d1  42062  primrootsunit1  42070  primrootscoprmpow  42072  primrootscoprbij  42075  remexz  42077  aks6d1c2p2  42092  hashscontpow1  42094  aks6d1c6isolem1  42147  aks6d1c6lem5  42150  unitscyglem5  42172  aks5lem8  42174  3rspcedvd  42188  oacl2g  43303  omcl2  43306  ofoaf  43328  dfno2  43401  clsk3nimkb  44013  clsk1indlem1  44018  ntrclsiso  44040  ntrclsk2  44041  ntrclskb  44042  ntrclsk3  44043  ntrclsk13  44044  ntrclsk4  44045  imo72b2lem0  44138  imo72b2lem2  44140  imo72b2lem1  44142  imo72b2  44145  mnuprdlem4  44248  mnuunid  44250  mnurndlem2  44255  restsubel  45131  fsupdm  46824  finfdm  46828  fsetsniunop  47034  fsetsnf  47036  cfsetsnfsetf  47043  cfsetsnfsetfo  47045  2reu8i  47098  mod0mul  47341  preimafvelsetpreimafv  47373  imasetpreimafvbijlemfo  47390  iccelpart  47418  fargshiftfo  47427  sprsymrelf1lem  47476  sprsymrelfo  47482  prproropf1o  47492  paireqne  47496  fmtnoodd  47518  fmtnoprmfac2lem1  47551  fmtnofac2lem  47553  fmtnofac2  47554  fmtnofac1  47555  41prothprm  47604  requad01  47606  dfodd6  47622  dfeven4  47623  opoeALTV  47668  opeoALTV  47669  nn0onn0exALTV  47684  nn0enn0exALTV  47685  nnennexALTV  47686  mogoldbblem  47705  sbgoldbst  47763  sgoldbeven3prm  47768  sbgoldbo  47772  nnsum3primesgbe  47777  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  evengpop3  47783  evengpoap3  47784  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  wtgoldbnnsum4prm  47787  bgoldbnnsum3prm  47789  bgoldbtbndlem4  47793  bgoldbtbnd  47794  bgoldbachlt  47798  tgoldbachlt  47801  predgclnbgrel  47824  clnbgredg  47825  clnbgrgrimlem  47918  grlimgredgex  47985  gpgprismgriedgdmss  48037  gpgedgvtx0  48046  gpgedgiov  48050  gpg3kgrtriexlem6  48073  gpg3kgrtriex  48074  uspgrsprfo  48133  1odd  48156  nnsgrpnmnd  48163  0even  48222  2even  48224  2zlidl  48225  2zrngamgm  48230  2zrngamnd  48232  2zrngagrp  48234  2zrngmmgm  48237  2zrngnmlid  48240  ply1mulgsumlem1  48372  ply1mulgsumlem2  48373  el0ldep  48452  nn0onn0ex  48509  nn0enn0ex  48510  nnennex  48511  nnpw2p  48572  1arymaptfo  48629  2arymaptfo  48640  eenglngeehlnmlem1  48723  eenglngeehlnmlem2  48724  rrx2vlinest  48727  itsclquadb  48762  iunlub  48806  iinglb  48807