Theorem rspcedvd 3567

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by:  rspcime  3570  fsnex  7231  updjud  9849  modfzo0difsn  13896  ssnn0fi  13938  fsuppmapnn0fiubex  13945  tpfo  14453  wrdl1exs1  14567  cshimadifsn0  14783  reusq0  15418  divconjdvds  16275  2tp1odd  16312  dfgcd2  16506  fissn0dvds  16579  ncoprmlnprm  16689  dvdsprmpweq  16846  oddprmdvds  16865  prmgaplem2  17012  prmgaplcmlem2  17014  prmgaplem5  17017  prmgapprmolem  17023  fullestrcsetc  18108  equivestrcsetc  18109  fullsetcestrc  18123  isnsgrp  18682  efmndmnd  18848  smndex1mnd  18872  smndex1n0mnd  18874  mgmnsgrpex  18893  sgrpnmndex  18894  dfgrp2  18929  grplrinv  18963  grpidinv  18965  dfgrp3  19006  cycsubmcl  19167  cycsubm  19168  ghmquskerlem1  19249  ringid  20246  ringadd2  20248  ringunitnzdiv  20369  rngisomring  20438  rngqiprngimfo  21291  ring2idlqus  21299  pzriprnglem10  21480  pzriprnglem11  21481  cply1coe0bi  22277  evls1maprnss  22353  scmatid  22489  scmataddcl  22491  scmatsubcl  22492  scmatmulcl  22493  scmatrhmcl  22503  mat0scmat  22513  symgmatr01lem  22628  cpmatacl  22691  cpmatinvcl  22692  m2cpmfo  22731  pmatcollpw3fi1lem2  22762  gausslemma2dlem1a  27342  2lgslem1b  27369  addsq2reu  27417  addsqrexnreu  27419  addsq2nreurex  27421  2sqreulem1  27423  2sqreunnlem1  27426  islnoppd  28822  outpasch  28837  hlpasch  28838  colopp  28851  colhp  28852  isinagd  28921  inaghl  28927  isleagd  28930  f1otrg  28953  usgredg4  29300  nbupgr  29427  nbumgrvtx  29429  nbgr2vtx1edg  29433  nbuhgr2vtx1edgb  29435  nbusgredgeu  29449  cusgrexilem2  29525  wlkvtxiedg  29708  elwwlks2ons3  30038  umgr2cwwkdifex  30150  1pthon2ve  30239  numclwwlk1lem2fo  30443  2ndimaxp  32734  1stpreimas  32794  swrdrn3  33030  cshwrnid  33036  gsummpt2d  33125  gsumhashmul  33143  cyc3genpmlem  33227  cyc3genpm  33228  cycpmconjs  33232  cyc3conja  33233  elrgspnlem1  33318  elrgspnsubrunlem2  33324  erlbrd  33339  erler  33341  rloccring  33346  fldgenval  33388  dvdsruassoi  33459  dvdsruasso  33460  lsmsnidl  33474  grplsmid  33479  quslsm  33480  nsgmgc  33487  nsgqusf1olem1  33488  nsgqusf1olem2  33489  nsgqusf1olem3  33490  elrspunidl  33503  elrspunsn  33504  mxidlprm  33545  mxidlirredi  33546  qsdrngilem  33569  1arithidom  33612  fedgmul  33791  ccfldextdgrr  33832  fldextrspunlsplem  33833  irngss  33847  irngnzply1lem  33850  constrsslem  33901  constrconj  33905  constrfiss  33911  constrllcllem  33912  constrlccllem  33913  constrcccllem  33914  nn0constr  33921  ist0cld  33993  zarclsun  34030  zarclsint  34032  zarcmplem  34041  rhmpreimacn  34045  esum2d  34253  reprsuc  34775  reprpmtf1o  34786  fmlasuc  35584  fmla1  35585  satffunlem1lem2  35601  satffunlem2lem2  35604  sategoelfvb  35617  2goelgoanfmla1  35622  unblimceq0lem  36782  unblimceq0  36783  unbdqndv2  36787  knoppndvlem19  36806  aks4d1  42542  primrootsunit1  42550  primrootscoprmpow  42552  primrootscoprbij  42555  remexz  42557  aks6d1c2p2  42572  hashscontpow1  42574  aks6d1c6isolem1  42627  aks6d1c6lem5  42630  unitscyglem5  42652  aks5lem8  42654  3rspcedvd  42671  oacl2g  43776  omcl2  43779  ofoaf  43801  dfno2  43873  clsk3nimkb  44485  clsk1indlem1  44490  ntrclsiso  44512  ntrclsk2  44513  ntrclskb  44514  ntrclsk3  44515  ntrclsk13  44516  ntrclsk4  44517  imo72b2lem0  44610  imo72b2lem2  44612  imo72b2lem1  44614  imo72b2  44617  mnuprdlem4  44720  mnuunid  44722  mnurndlem2  44727  restsubel  45601  fsupdm  47288  finfdm  47292  fsetsniunop  47509  fsetsnf  47511  cfsetsnfsetf  47518  cfsetsnfsetfo  47520  2reu8i  47573  mod0mul  47822  nndivides2  47844  preimafvelsetpreimafv  47860  imasetpreimafvbijlemfo  47877  iccelpart  47905  fargshiftfo  47914  sprsymrelf1lem  47963  sprsymrelfo  47969  prproropf1o  47979  paireqne  47983  nprmmul3  48001  fmtnoodd  48008  fmtnoprmfac2lem1  48041  fmtnofac2lem  48043  fmtnofac2  48044  fmtnofac1  48045  41prothprm  48094  requad01  48109  dfodd6  48125  dfeven4  48126  opoeALTV  48171  opeoALTV  48172  nn0onn0exALTV  48187  nn0enn0exALTV  48188  nnennexALTV  48189  mogoldbblem  48208  sbgoldbst  48266  sgoldbeven3prm  48271  sbgoldbo  48275  nnsum3primesgbe  48280  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  evengpop3  48286  evengpoap3  48287  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  bgoldbtbndlem4  48296  bgoldbtbnd  48297  bgoldbachlt  48301  tgoldbachlt  48304  predgclnbgrel  48327  clnbgredg  48328  clnbgrgrimlem  48421  grlimgredgex  48488  gpgprismgriedgdmss  48540  gpgedgvtx0  48549  gpgedgiov  48553  gpg3kgrtriexlem6  48576  gpg3kgrtriex  48577  uspgrsprfo  48636  1odd  48659  nnsgrpnmnd  48666  0even  48725  2even  48727  2zlidl  48728  2zrngamgm  48733  2zrngamnd  48735  2zrngagrp  48737  2zrngmmgm  48740  2zrngnmlid  48743  ply1mulgsumlem1  48874  ply1mulgsumlem2  48875  el0ldep  48954  nn0onn0ex  49011  nn0enn0ex  49012  nnennex  49013  nnpw2p  49074  1arymaptfo  49131  2arymaptfo  49142  eenglngeehlnmlem1  49225  eenglngeehlnmlem2  49226  rrx2vlinest  49229  itsclquadb  49264  iunlub  49308  iinglb  49309