Theorem rspcedvd 3563

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070

This theorem is referenced by:  rspcime  3564  rspcedeq1vd  3566  rspcedeq2vd  3567  elpr2elpr  4800  prproe  4838  fsnex  7148  fsetfocdm  8637  updjud  9680  negfi  11912  elpq  12703  reltre  13062  rpltrp  13063  reltxrnmnf  13064  modmuladd  13621  modmuladdnn0  13623  modfzo0difsn  13651  ssnn0fi  13693  fsuppmapnn0fiubex  13700  wrdl1exs1  14306  cshimadifsn0  14531  reusq0  15162  divconjdvds  16012  2tp1odd  16049  dfgcd2  16242  fissn0dvds  16312  ncoprmlnprm  16420  dvdsprmpweq  16573  oddprmdvds  16592  prmgaplem2  16739  prmgaplcmlem2  16741  prmgaplem5  16744  prmgapprmolem  16750  fullestrcsetc  17856  equivestrcsetc  17857  fullsetcestrc  17871  isnsgrp  18367  efmndmnd  18516  smndex1mnd  18537  smndex1n0mnd  18539  mgmnsgrpex  18558  sgrpnmndex  18559  dfgrp2  18592  grplrinv  18621  grpidinv  18623  dfgrp3  18662  cycsubmcl  18808  cycsubm  18809  ringid  19801  cply1coe0bi  21459  scmatid  21651  scmataddcl  21653  scmatsubcl  21654  scmatmulcl  21655  scmatrhmcl  21665  mat0scmat  21675  symgmatr01lem  21790  cpmatacl  21853  cpmatinvcl  21854  m2cpmfo  21893  pmatcollpw3fi1lem2  21924  gausslemma2dlem1a  26501  2lgslem1b  26528  addsq2reu  26576  addsqrexnreu  26578  addsq2nreurex  26580  2sqreulem1  26582  2sqreunnlem1  26585  islnoppd  27089  outpasch  27104  hlpasch  27105  colopp  27118  colhp  27119  isinagd  27188  inaghl  27194  isleagd  27197  f1otrg  27220  usgredg4  27572  nbupgr  27699  nbumgrvtx  27701  nbgr2vtx1edg  27705  nbuhgr2vtx1edgb  27707  nbusgredgeu  27721  cusgrexilem2  27797  wlkvtxiedg  27979  elwwlks2ons3  28306  umgr2cwwkdifex  28415  1pthon2ve  28504  numclwwlk1lem2fo  28708  2ndimaxp  30970  1stpreimas  31024  swrdrn3  31213  cshwrnid  31219  gsummpt2d  31295  gsumhashmul  31302  cyc3genpmlem  31404  cyc3genpm  31405  cycpmconjs  31409  cyc3conja  31410  lsmsnidl  31573  grplsmid  31578  quslsm  31579  nsgmgc  31583  nsgqusf1olem1  31584  nsgqusf1olem2  31585  nsgqusf1olem3  31586  elrspunidl  31592  mxidlprm  31626  fedgmul  31698  ccfldextdgrr  31728  ist0cld  31769  zarclsun  31806  zarclsint  31808  zarcmplem  31817  rhmpreimacn  31821  esum2d  32047  reprsuc  32581  reprpmtf1o  32592  fmlasuc  33334  fmla1  33335  satffunlem1lem2  33351  satffunlem2lem2  33354  sategoelfvb  33367  2goelgoanfmla1  33372  unblimceq0lem  34672  unblimceq0  34673  unbdqndv2  34677  knoppndvlem19  34696  aks4d1  40083  3rspcedvd  40168  fsuppind  40265  nnn1suc  40282  sn-negex12  40384  prjspertr  40430  prjsperref  40431  prjspersym  40432  prjspvs  40435  0prjspnrel  40450  clsk3nimkb  41609  clsk1indlem1  41614  ntrclsiso  41636  ntrclsk2  41637  ntrclskb  41638  ntrclsk3  41639  ntrclsk13  41640  ntrclsk4  41641  imo72b2lem0  41735  imo72b2lem2  41737  imo72b2lem1  41739  imo72b2  41742  mnuprdlem4  41852  mnuunid  41854  mnurndlem2  41859  fsetsniunop  44499  fsetsnf  44501  cfsetsnfsetf  44508  cfsetsnfsetfo  44510  2reu8i  44561  preimafvelsetpreimafv  44796  imasetpreimafvbijlemfo  44813  iccelpart  44841  fargshiftfo  44850  sprsymrelf1lem  44899  sprsymrelfo  44905  prproropf1o  44915  paireqne  44919  fmtnoodd  44941  fmtnoprmfac2lem1  44974  fmtnofac2lem  44976  fmtnofac2  44977  fmtnofac1  44978  41prothprm  45027  requad01  45029  dfodd6  45045  dfeven4  45046  opoeALTV  45091  opeoALTV  45092  nn0onn0exALTV  45107  nn0enn0exALTV  45108  nnennexALTV  45109  mogoldbblem  45128  sbgoldbst  45186  sgoldbeven3prm  45191  sbgoldbo  45195  nnsum3primesgbe  45200  nnsum4primesodd  45204  nnsum4primesoddALTV  45205  evengpop3  45206  evengpoap3  45207  nnsum4primeseven  45208  nnsum4primesevenALTV  45209  wtgoldbnnsum4prm  45210  bgoldbnnsum3prm  45212  bgoldbtbndlem4  45216  bgoldbtbnd  45217  bgoldbachlt  45221  tgoldbachlt  45224  isomuspgrlem2d  45239  uspgrsprfo  45266  1odd  45321  nnsgrpnmnd  45328  0even  45445  2even  45447  2zlidl  45448  2zrngamgm  45453  2zrngamnd  45455  2zrngagrp  45457  2zrngmmgm  45460  2zrngnmlid  45463  ply1mulgsumlem1  45683  ply1mulgsumlem2  45684  el0ldep  45763  mod0mul  45821  nn0onn0ex  45825  nn0enn0ex  45826  nnennex  45827  nnpw2p  45888  1arymaptfo  45945  2arymaptfo  45956  eenglngeehlnmlem1  46039  eenglngeehlnmlem2  46040  rrx2vlinest  46043  itsclquadb  46078