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 16	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089

This theorem is used by:  rspcime  3584  fsnex  7288  updjud  9943  modfzo0difsn  14011  ssnn0fi  14053  fsuppmapnn0fiubex  14060  tpfo  14569  wrdl1exs1  14685  swrdrn3  14726  cshimadifsn0  14905  reusq0  15556  divconjdvds  16411  2tp1odd  16448  dfgcd2  16642  fissn0dvds  16715  ncoprmlnprm  16825  dvdsprmpweq  16982  oddprmdvds  17001  prmgaplem2  17148  prmgaplcmlem2  17150  prmgaplem5  17153  prmgapprmolem  17159  fullestrcsetc  18245  equivestrcsetc  18246  fullsetcestrc  18260  isnsgrp  18831  efmndmnd  19004  smndex1mnd  19028  smndex1n0mnd  19030  mgmnsgrpex  19049  sgrpnmndex  19050  dfgrp2  19092  grplrinv  19126  grpidinv  19128  dfgrp3  19168  cycsubmcl  19335  cycsubm  19336  ghmquskerlem1  19416  ringid  20421  ringadd2  20423  ringunitnzdiv  20545  rngisomring  20614  rngqiprngimfo  21510  ring2idlqus  21518  pzriprnglem10  21709  pzriprnglem11  21710  cply1coe0bi  22533  evls1maprnss  22609  scmatid  22742  scmataddcl  22744  scmatsubcl  22745  scmatmulcl  22746  scmatrhmcl  22756  mat0scmat  22766  symgmatr01lem  22881  cpmatacl  22947  cpmatinvcl  22948  m2cpmfo  22987  pmatcollpw3fi1lem2  23018  gausslemma2dlem1a  27609  2lgslem1b  27636  addsq2reu  27684  addsqrexnreu  27686  addsq2nreurex  27688  2sqreulem1  27690  2sqreunnlem1  27693  islnoppd  29103  outpasch  29120  hlpasch  29121  colopp  29134  colhp  29135  isinagd  29245  inaghl  29251  isleagd  29254  f1otrg  29335  usgredg4  29685  nbupgr  29812  nbumgrvtx  29814  nbgr2vtx1edg  29818  nbuhgr2vtx1edgb  29820  nbusgredgeu  29834  cusgrexilem2  29910  wlkvtxiedg  30092  elwwlks2ons3  30431  umgr2cwwkdifex  30543  1pthon2ve  30642  numclwwlk1lem2fo  30846  2ndimaxp  33127  1stpreimas  33186  cshwrnid  33409  gsummpt2d  33497  gsumhashmul  33515  cyc3genpmlem  33599  cyc3genpm  33600  cycpmconjs  33604  cyc3conja  33605  elrgspnlem1  33690  elrgspnsubrunlem2  33696  erlbrd  33711  erler  33713  rloccring  33719  rlocisunit  33724  fldgenval  33761  dvdsruassoi  33825  dvdsruasso  33826  lsmsnidl  33838  grplsmid  33841  quslsm  33842  nsgmgc  33849  nsgqusf1olem1  33850  nsgqusf1olem2  33851  nsgqusf1olem3  33852  elrspunidl  33864  elrspunsn  33865  mxidlprm  33881  qsdrngilem  33904  1arithidom  33955  fedgmul  34149  ccfldextdgrr  34190  fldextrspunlsplem  34191  irngss  34205  irngnzply1lem  34208  constrsslem  34259  constrconj  34263  constrfiss  34269  constrllcllem  34270  constrlccllem  34271  constrcccllem  34272  nn0constr  34279  ist0cld  34351  zarclsun  34388  zarclsint  34390  zarcmplem  34399  rhmpreimacn  34403  esum2d  34611  reprsuc  35131  reprpmtf1o  35142  fmlasuc  35973  fmla1  35974  satffunlem1lem2  35990  satffunlem2lem2  35993  sategoelfvb  36006  2goelgoanfmla1  36011  unblimceq0lem  37211  unblimceq0  37212  unbdqndv2  37216  knoppndvlem19  37235  aks4d1  42963  primrootsunit1  42971  primrootscoprmpow  42973  primrootscoprbij  42976  remexz  42978  aks6d1c2p2  42993  hashscontpow1  42995  aks6d1c6isolem1  43048  aks6d1c6lem5  43051  unitscyglem5  43073  aks5lem8  43075  3rspcedvd  43094  oacl2g  44179  omcl2  44182  ofoaf  44204  dfno2  44276  clsk3nimkb  44888  clsk1indlem1  44893  ntrclsiso  44915  ntrclsk2  44916  ntrclskb  44917  ntrclsk3  44918  ntrclsk13  44919  ntrclsk4  44920  imo72b2lem0  45013  imo72b2lem2  45015  imo72b2lem1  45017  imo72b2  45020  mnuprdlem4  45107  mnuunid  45109  mnurndlem2  45114  restsubel  45993  fsupdm  47678  finfdm  47682  fsetsniunop  47945  fsetsnf  47947  cfsetsnfsetf  47954  cfsetsnfsetfo  47956  2reu8i  48009  mod0mul  48258  nndivides2  48280  preimafvelsetpreimafv  48296  imasetpreimafvbijlemfo  48313  iccelpart  48341  fargshiftfo  48350  sprsymrelf1lem  48399  sprsymrelfo  48405  prproropf1o  48415  paireqne  48419  nprmmul3  48437  fmtnoodd  48444  fmtnoprmfac2lem1  48477  fmtnofac2lem  48479  fmtnofac2  48480  fmtnofac1  48481  41prothprm  48530  requad01  48545  dfodd6  48561  dfeven4  48562  opoeALTV  48607  opeoALTV  48608  nn0onn0exALTV  48623  nn0enn0exALTV  48624  nnennexALTV  48625  mogoldbblem  48644  sbgoldbst  48702  sgoldbeven3prm  48707  sbgoldbo  48711  nnsum3primesgbe  48716  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  evengpop3  48722  evengpoap3  48723  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  wtgoldbnnsum4prm  48726  bgoldbnnsum3prm  48728  bgoldbtbndlem4  48732  bgoldbtbnd  48733  bgoldbachlt  48737  tgoldbachlt  48740  predgclnbgrel  48763  clnbgredg  48764  clnbgrgrimlem  48857  grlimgredgex  48924  gpgprismgriedgdmss  48976  gpgedgvtx0  48985  gpgedgiov  48989  gpg3kgrtriexlem6  49012  gpg3kgrtriex  49013  uspgrsprfo  49072  1odd  49094  nnsgrpnmnd  49101  0even  49160  2even  49162  2zlidl  49163  2zrngamgm  49168  2zrngamnd  49170  2zrngagrp  49172  2zrngmmgm  49175  2zrngnmlid  49178  ply1mulgsumlem1  49324  ply1mulgsumlem2  49325  el0ldep  49404  nn0onn0ex  49461  nn0enn0ex  49462  nnennex  49463  nnpw2p  49524  1arymaptfo  49581  2arymaptfo  49592  eenglngeehlnmlem1  49675  eenglngeehlnmlem2  49676  rrx2vlinest  49679  itsclquadb  49714  iunlub  49757  iinglb  49758