Theorem rspcedvd 3564

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

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

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071

This theorem is referenced by:  rspcime  3565  rspcedeq1vd  3567  rspcedeq2vd  3568  elpr2elpr  4800  prproe  4838  fsnex  7164  fsetfocdm  8658  updjud  9701  negfi  11933  elpq  12724  reltre  13083  rpltrp  13084  reltxrnmnf  13085  modmuladd  13642  modmuladdnn0  13644  modfzo0difsn  13672  ssnn0fi  13714  fsuppmapnn0fiubex  13721  wrdl1exs1  14327  cshimadifsn0  14552  reusq0  15183  divconjdvds  16033  2tp1odd  16070  dfgcd2  16263  fissn0dvds  16333  ncoprmlnprm  16441  dvdsprmpweq  16594  oddprmdvds  16613  prmgaplem2  16760  prmgaplcmlem2  16762  prmgaplem5  16765  prmgapprmolem  16771  fullestrcsetc  17877  equivestrcsetc  17878  fullsetcestrc  17892  isnsgrp  18388  efmndmnd  18537  smndex1mnd  18558  smndex1n0mnd  18560  mgmnsgrpex  18579  sgrpnmndex  18580  dfgrp2  18613  grplrinv  18642  grpidinv  18644  dfgrp3  18683  cycsubmcl  18829  cycsubm  18830  ringid  19822  cply1coe0bi  21480  scmatid  21672  scmataddcl  21674  scmatsubcl  21675  scmatmulcl  21676  scmatrhmcl  21686  mat0scmat  21696  symgmatr01lem  21811  cpmatacl  21874  cpmatinvcl  21875  m2cpmfo  21914  pmatcollpw3fi1lem2  21945  gausslemma2dlem1a  26522  2lgslem1b  26549  addsq2reu  26597  addsqrexnreu  26599  addsq2nreurex  26601  2sqreulem1  26603  2sqreunnlem1  26606  islnoppd  27110  outpasch  27125  hlpasch  27126  colopp  27139  colhp  27140  isinagd  27209  inaghl  27215  isleagd  27218  f1otrg  27241  usgredg4  27593  nbupgr  27720  nbumgrvtx  27722  nbgr2vtx1edg  27726  nbuhgr2vtx1edgb  27728  nbusgredgeu  27742  cusgrexilem2  27818  wlkvtxiedg  28001  elwwlks2ons3  28329  umgr2cwwkdifex  28438  1pthon2ve  28527  numclwwlk1lem2fo  28731  2ndimaxp  30993  1stpreimas  31047  swrdrn3  31236  cshwrnid  31242  gsummpt2d  31318  gsumhashmul  31325  cyc3genpmlem  31427  cyc3genpm  31428  cycpmconjs  31432  cyc3conja  31433  lsmsnidl  31596  grplsmid  31601  quslsm  31602  nsgmgc  31606  nsgqusf1olem1  31607  nsgqusf1olem2  31608  nsgqusf1olem3  31609  elrspunidl  31615  mxidlprm  31649  fedgmul  31721  ccfldextdgrr  31751  ist0cld  31792  zarclsun  31829  zarclsint  31831  zarcmplem  31840  rhmpreimacn  31844  esum2d  32070  reprsuc  32604  reprpmtf1o  32615  fmlasuc  33357  fmla1  33358  satffunlem1lem2  33374  satffunlem2lem2  33377  sategoelfvb  33390  2goelgoanfmla1  33395  unblimceq0lem  34695  unblimceq0  34696  unbdqndv2  34700  knoppndvlem19  34719  aks4d1  40104  3rspcedvd  40189  fsuppind  40286  nnn1suc  40303  sn-negex12  40405  prjspertr  40451  prjsperref  40452  prjspersym  40453  prjspvs  40456  0prjspnrel  40471  clsk3nimkb  41657  clsk1indlem1  41662  ntrclsiso  41684  ntrclsk2  41685  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  ntrclsk4  41689  imo72b2lem0  41783  imo72b2lem2  41785  imo72b2lem1  41787  imo72b2  41790  mnuprdlem4  41900  mnuunid  41902  mnurndlem2  41907  fsetsniunop  44554  fsetsnf  44556  cfsetsnfsetf  44563  cfsetsnfsetfo  44565  2reu8i  44616  preimafvelsetpreimafv  44851  imasetpreimafvbijlemfo  44868  iccelpart  44896  fargshiftfo  44905  sprsymrelf1lem  44954  sprsymrelfo  44960  prproropf1o  44970  paireqne  44974  fmtnoodd  44996  fmtnoprmfac2lem1  45029  fmtnofac2lem  45031  fmtnofac2  45032  fmtnofac1  45033  41prothprm  45082  requad01  45084  dfodd6  45100  dfeven4  45101  opoeALTV  45146  opeoALTV  45147  nn0onn0exALTV  45162  nn0enn0exALTV  45163  nnennexALTV  45164  mogoldbblem  45183  sbgoldbst  45241  sgoldbeven3prm  45246  sbgoldbo  45250  nnsum3primesgbe  45255  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  evengpop3  45261  evengpoap3  45262  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  bgoldbtbndlem4  45271  bgoldbtbnd  45272  bgoldbachlt  45276  tgoldbachlt  45279  isomuspgrlem2d  45294  uspgrsprfo  45321  1odd  45376  nnsgrpnmnd  45383  0even  45500  2even  45502  2zlidl  45503  2zrngamgm  45508  2zrngamnd  45510  2zrngagrp  45512  2zrngmmgm  45515  2zrngnmlid  45518  ply1mulgsumlem1  45738  ply1mulgsumlem2  45739  el0ldep  45818  mod0mul  45876  nn0onn0ex  45880  nn0enn0ex  45881  nnennex  45882  nnpw2p  45943  1arymaptfo  46000  2arymaptfo  46011  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  rrx2vlinest  46098  itsclquadb  46133