MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspcev Structured version   Visualization version   GIF version

Theorem rspcev 3620
Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2136, ax-11 2151, ax-12 2167. (Revised by SN, 12-Dec-2023.)
Hypothesis
Ref Expression
rspcv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspcev ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcev
StepHypRef Expression
1 id 22 . . 3 (𝐴𝐵𝐴𝐵)
2 rspcv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
32adantl 482 . . 3 ((𝐴𝐵𝑥 = 𝐴) → (𝜑𝜓))
41, 3rspcedv 3613 . 2 (𝐴𝐵 → (𝜓 → ∃𝑥𝐵 𝜑))
54imp 407 1 ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ral 3140  df-rex 3141
This theorem is referenced by:  rspceaimv  3625  rspc2ev  3632  rspc3ev  3634  rspceeqv  3635  reu6i  3716  rspesbca  3861  eliuni  4916  iuneqconst  4921  brralrspcev  5117  wefrc  5542  wereu2  5545  xpdifid  6018  onfr  6223  ordunidif  6232  eliman0  6698  dffv2  6749  elrnrexdm  6847  eldmrexrn  6849  elabrex  6993  f1elima  7012  fliftfun  7054  fliftval  7058  f1oiso2  7094  sorpssuni  7447  sorpssint  7448  onssmin  7501  onminex  7511  fimaproj  7818  tfrlem12  8014  seqomlem2  8076  oawordeulem  8169  oaass  8176  odi  8194  omass  8195  omeulem1  8197  oen0  8201  oelim2  8210  oeeulem  8216  nnawordex  8252  boxcutc  8493  snfi  8582  onfin  8697  pssnn  8724  ssnnfi  8725  dif1en  8739  findcard  8745  frfi  8751  fisupg  8754  nnsdomg  8765  unfi  8773  fissuni  8817  fipreima  8818  finsschain  8819  indexfi  8820  marypha1lem  8885  eqsup  8908  supmax  8919  fisup2g  8920  fisupcl  8921  supisoex  8926  infmin  8946  fiinfg  8951  fiinf2g  8952  wofib  8997  wemaplem2  8999  card2inf  9007  brwdom2  9025  cnfcom3clem  9156  trcl  9158  r1ordg  9195  r1pwss  9201  tz9.12lem3  9206  tz9.12  9207  r1elwf  9213  tcrank  9301  scottex  9302  scott0  9303  isnumi  9363  onsdom  9413  ondomen  9451  infpwfien  9476  cardaleph  9503  infenaleph  9505  alephfplem4  9521  alephfp2  9523  dfac2b  9544  ackbij1lem18  9647  ackbij1  9648  cflem  9656  cflecard  9663  cfsuc  9667  cfflb  9669  cofsmo  9679  coftr  9683  fin23lem7  9726  fin23lem11  9727  enfin2i  9731  fin23lem26  9735  isf32lem5  9767  isf34lem4  9787  isfin1-3  9796  fin1a2lem7  9816  axdc3lem4  9863  ttukeylem7  9925  iunfo  9949  ficard  9975  pwcfsdom  9993  fpwwe2lem12  10051  wunex  10149  eltsk2g  10161  grur1  10230  axgroth6  10238  inaprc  10246  nqereu  10339  archnq  10390  genpnmax  10417  ltexpri  10453  prlem936  10457  recexpr  10461  supexpr  10464  negexsr  10512  recexsrlem  10513  recexsr  10517  supsrlem  10521  axrnegex  10572  axrrecex  10573  axpre-sup  10579  1re  10629  dedekind  10791  dedekindle  10792  cnegex  10809  cnegex2  10810  recex  11260  receu  11273  cju  11622  nn2ge  11652  nominpos  11862  zdiv  12040  btwnz  12072  uzwo  12299  ublbneg  12321  lbzbi  12324  zsupss  12325  uzsupss  12328  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem4  12367  rpnnen1lem5  12368  z2ge  12579  qbtwnre  12580  qbtwnxr  12581  xralrple  12586  xrsupsslem  12688  xrinfmsslem  12689  supxrpnf  12699  icc0  12774  uzsup  13219  expnbnd  13581  expmulnbnd  13584  hashkf  13680  hashdom  13728  iswrdi  13853  rtrclreclem1  14405  rtrclreclem2  14406  rtrclreclem3  14407  01sqrex  14597  resqrex  14598  sqrtneg  14615  abs1m  14683  rexanuz  14693  rexuz3  14696  rexuzre  14700  sqreu  14708  o1lo1  14882  climconst  14888  rlimclim1  14890  climshftlem  14919  rlimo1  14961  lo1add  14971  lo1mul  14972  lo1le  14996  isercoll  15012  serf0  15025  zsum  15063  fsum  15065  fsumcvg3  15074  mertenslem1  15228  ntrivcvgn0  15242  ntrivcvgmullem  15245  zprod  15279  fprod  15283  fprodntriv  15284  dvdsval2  15598  dvds0lem  15608  dvds1lem  15609  dvds2lem  15610  odd2np1lem  15677  odd2np1  15678  opeo  15702  omeo  15703  divalglem9  15740  gcdcllem3  15838  lcmcllem  15928  qredeu  15990  exprmfct  16036  isprm5  16039  odzcllem  16117  reumodprminv  16129  modprm0  16130  nnnn0modprm0  16131  pythagtriplem19  16158  pcprmpw2  16206  pockthi  16231  infpnlem2  16235  vdwlem2  16306  vdwlem10  16314  vdwlem13  16317  ramub1lem1  16350  cshwrepswhash1  16424  imasleval  16802  mreexexlem3d  16905  mreexexlem4d  16906  iscatd  16932  poslubd  17746  fpwipodrs  17762  ismgmid2  17866  mgmidsssn0  17870  gsumval2a  17883  ismndd  17921  isgrpd2  18061  isgrpd  18063  imasgrp2  18152  mhmmnd  18159  ghmgrp  18161  gaorber  18376  orbsta  18381  cayleyth  18472  pmtrdifel  18537  pmtrdifwrdel  18542  pmtrdifwrdel2  18543  psgnunilem2  18552  psgnunilem3  18553  psgnvalii  18566  pgpfi1  18649  sylow1lem3  18654  sylow1lem5  18656  pgpfi  18659  sylow2alem2  18672  efgredeu  18807  lt6abl  18944  pgpfac1lem3a  19127  pgpfac1lem3  19128  pgpfac1lem5  19130  pgpfaclem1  19132  pgpfaclem3  19134  ablfaclem2  19137  dvdsrmul  19327  dvdsr01  19334  irredrmul  19386  lspf  19675  lspval  19676  lssats2  19701  lspfixed  19829  lspsolvlem  19843  aspval  20030  evlseu  20224  zringlpir  20564  zncyg  20623  cygth  20646  frlmup4  20873  fiinbas  21488  topbas  21508  pptbas  21544  clsval  21573  elcls  21609  neiint  21640  neips  21649  opnneissb  21650  opnssneib  21651  innei  21661  neiptopnei  21668  restbas  21694  neitr  21716  pnfnei  21756  mnfnei  21757  lmconst  21797  iscnp4  21799  cncnpi  21814  cnconst2  21819  cnprest  21825  cnpdis  21829  nrmsep  21893  regsep2  21912  cmpcovf  21927  cmpsub  21936  cmpcld  21938  hauscmplem  21942  conncompid  21967  2ndci  21984  2ndcsb  21985  2ndc1stc  21987  1stcrest  21989  2ndcctbss  21991  2ndcdisj  21992  2ndcomap  21994  2ndcsep  21995  dis2ndc  21996  restlly  22019  islly2  22020  hausllycmp  22030  cldllycmp  22031  lly1stc  22032  dislly  22033  ssref  22048  refref  22049  finlocfin  22056  dissnlocfin  22065  locfindis  22066  llycmpkgen2  22086  cmpkgen  22087  1stckgenlem  22089  elptr  22109  ptbasfi  22117  neitx  22143  ptpjopn  22148  txcnp  22156  ptcnplem  22157  txlly  22172  txnlly  22173  txtube  22176  txcmplem1  22177  tx1stc  22186  txkgen  22188  xkococnlem  22195  txconn  22225  tgqtop  22248  kqreglem1  22277  kqreglem2  22278  kqnrmlem1  22279  kqnrmlem2  22280  reghmph  22329  nrmhmph  22330  fbssfi  22373  opnfbas  22378  isfil2  22392  fsubbas  22403  ssfg  22408  fgss2  22410  fbasrn  22420  filuni  22421  fgtr  22426  ssufl  22454  uffix  22457  elfm2  22484  elfm3  22486  imaelfm  22487  rnelfmlem  22488  rnelfm  22489  fmfnfmlem4  22493  fmfnfm  22494  fmco  22497  ufldom  22498  hausflim  22517  flimcls  22521  hauspwpwf1  22523  flffbas  22531  txflf  22542  fclscf  22561  fclsfnflim  22563  alexsubALTlem4  22586  alexsubALT  22587  tmdgsum2  22632  symgtgp  22637  subgntr  22642  opnsubg  22643  ghmcnp  22650  qustgpopn  22655  tsmsfbas  22663  tsmsxplem1  22688  ustexsym  22751  elrnust  22760  trust  22765  utoptop  22770  restutop  22773  restutopopn  22774  ustuqtop4  22780  utopsnneiplem  22783  iducn  22819  fmucnd  22828  cfilufg  22829  trcfilu  22830  neipcfilu  22832  imasdsf1olem  22910  blssps  22961  blss  22962  blssexps  22963  blssex  22964  ssblex  22965  blin2  22966  neibl  23038  blcld  23042  metss2  23049  stdbdmopn  23055  met1stc  23058  met2ndci  23059  metrest  23061  prdsxmslem2  23066  metcnp3  23077  metuval  23086  metustexhalf  23093  metustfbas  23094  cfilucfil  23096  restmetu  23107  dscopn  23110  ngptgp  23172  nlmvscnlem1  23222  tgioo  23331  tgqioo  23335  xrsmopn  23347  zcld  23348  recld2  23349  zdis  23351  icccmplem1  23357  icccmplem2  23358  xmetdcn2  23372  addcnlem  23399  xrhmeo  23477  cnheibor  23486  cnllycmp  23487  lebnumlem3  23494  lebnum  23495  xlebnum  23496  lebnumii  23497  elpi1i  23577  ipcnlem1  23775  lmnn  23793  iscfil3  23803  cfilres  23826  flimcfil  23844  bcthlem4  23857  bcthlem5  23858  minveclem4c  23955  minveclem2  23956  minveclem3b  23958  minveclem3  23959  minveclem4  23962  minveclem6  23964  ivthlem2  23980  ivth  23982  ivthle  23984  ivthle2  23985  elovolmr  24004  ovolunlem1  24025  ovoliunlem2  24031  ovolicc1  24044  iundisj  24076  iunmbl2  24085  dyadmbllem  24127  volivth  24135  mbflimsup  24194  i1faddlem  24221  i1fmullem  24222  itg2lr  24258  itg2monolem1  24278  limcnlp  24403  ellimc3  24404  limcflf  24406  limciun  24419  rollelem  24513  c1lip1  24521  lhop1lem  24537  ply1divex  24657  ig1peu  24692  elply2  24713  coeeq  24744  plydivlem3  24811  plydivlem4  24812  elqaalem3  24837  qaa  24839  iaa  24841  aareccl  24842  aannenlem2  24845  aalioulem2  24849  aalioulem3  24850  aalioulem5  24852  aalioulem6  24853  aaliou  24854  aaliou2  24856  aaliou3lem8  24861  ulmshftlem  24904  reeff1o  24962  pilem2  24967  pilem3  24968  efif1olem2  25054  efopn  25168  cxpcn3lem  25255  cxpeq  25265  dcubic2  25349  quart  25366  xrlimcnp  25473  ftalem5  25581  ftalem7  25583  sgmnncl  25651  dvdsppwf1o  25690  musum  25695  perfect  25734  dchrptlem1  25767  dchrptlem2  25768  dchrpt  25770  bpos1lem  25785  lgsqrlem4  25852  lgsdchrval  25857  2sqblem  25934  dchrisumlem3  25994  chpdifbndlem2  26057  pntrsumbnd2  26070  pntpbnd1  26089  pntpbnd2  26090  pntpbnd  26091  pntibndlem2  26094  pntibndlem3  26095  pntleme  26111  pntlem3  26112  axtgcont  26182  tgcgrxfr  26231  legid  26300  btwnleg  26301  leg0  26305  tghilberti1  26350  tglnpt2  26354  colline  26362  mirreu3  26367  isperp2  26428  colperpex  26446  lnopp2hpgb  26476  hpgerlem  26478  brbtwn  26612  brcgr  26613  brbtwn2  26618  axpasch  26654  axlowdimlem14  26668  axlowdim2  26673  axcontlem2  26678  axcontlem4  26680  axcontlem8  26684  axcontlem10  26686  axcontlem12  26688  fusgrn0degnn0  27208  friendshipgt3  28104  lpni  28184  isgrpoi  28202  vacn  28398  smcnlem  28401  nmosetn0  28469  nmoolb  28475  nmobndi  28479  nmoo0  28495  nmlno0lem  28497  isblo3i  28505  blo3i  28506  blocnilem  28508  ubthlem1  28574  minvecolem2  28579  minvecolem3  28580  minvecolem4c  28583  minvecolem4  28584  minvecolem5  28585  minvecolem6  28586  norm1exi  28954  occl  29008  spanval  29037  spancl  29040  shsval2i  29091  ococin  29112  pjoml6i  29293  nmopsetn0  29569  nmfnsetn0  29582  nmoplb  29611  nmfnlb  29628  nmop0  29690  nmfn0  29691  nmlnop0iALT  29699  nmopun  29718  nmcexi  29730  lnconi  29737  lnopcnbd  29740  lnfncnbd  29761  riesz3i  29766  riesz1  29769  cnlnadjlem2  29772  cnlnadjlem8  29778  cnlnadjlem9  29779  adjbd1o  29789  branmfn  29809  opsqrlem1  29844  pjnmopi  29852  strlem1  29954  stri  29961  hstri  29969  cvcon3  29988  cvnbtwn  29990  superpos  30058  shatomici  30062  atcvat4i  30101  mdsymlem2  30108  cdj1i  30137  cdj3i  30145  rexunirn  30183  foresf1o  30192  iundisjf  30267  elunirn2  30324  aciunf1lem  30335  fnpreimac  30344  fgreu  30345  fcnvgreu  30346  xrge0infss  30410  ssnnssfz  30436  iundisjfi  30445  xreceu  30525  rexdiv  30529  isarchi3  30743  archirngz  30745  archiabllem2a  30750  rhmdvdsr  30818  0nellinds  30862  qtophaus  30999  reff  31002  locfinreflem  31003  cmpcref  31013  dispcmp  31022  metidval  31029  pstmval  31034  tpr2rico  31054  pnfneige0  31093  qqhucn  31132  rrhre  31161  indf1ofs  31184  esumcst  31221  esumpcvgval  31236  dmsigagen  31302  rossros  31338  dya2icoseg  31434  dya2iocnrect  31438  dya2iocuni  31440  eulerpartlemgvv  31533  dstfrvunirn  31631  ballotlem4  31655  ballotlemic  31663  ballotlem1c  31664  ballotlemrc  31687  signsw0g  31725  signswmnd  31726  prodfzo03  31773  tgoldbachgt  31833  loop1cycl  32281  umgr2cycllem  32284  umgr2cycl  32285  subfacp1lem3  32326  erdsze2lem2  32348  cnpconn  32374  txpconn  32376  ptpconn  32377  indispconn  32378  connpconn  32379  cvxpconn  32386  cnllysconn  32389  cvmsss2  32418  cvmcov2  32419  cvmopnlem  32422  cvmliftlem14  32441  cvmliftlem15  32442  cvmlift2lem11  32457  cvmlift2lem12  32458  cvmlift2lem13  32459  cvmlift3lem2  32464  cvmlift3lem6  32468  cvmlift3lem9  32471  mthmi  32721  br8  32889  br6  32890  br4  32891  dfon2lem9  32933  trpredtr  32966  dftrpred3g  32969  frpomin  32975  frmin  32981  poseq  32992  wzel  33008  wsuclem  33009  wsuclb  33012  elno2  33058  sltval2  33060  noreson  33064  sltres  33066  noseponlem  33068  nolesgn2o  33075  nodense  33093  nosupfv  33103  nosupres  33104  nosupbnd1lem3  33107  nosupbnd1lem5  33109  nosupbnd2lem1  33112  noetalem3  33116  noetalem5  33118  imagesset  33311  fvtransport  33390  brcolinear  33417  brsegle  33466  seglerflx  33470  seglemin  33471  btwnsegle  33475  fvray  33499  fvline  33502  hilbert1.1  33512  elhf2  33533  0hf  33535  nn0prpwlem  33567  nn0prpw  33568  fness  33594  fneref  33595  fnessref  33602  refssfne  33603  neibastop2lem  33605  fnemeet1  33611  tailfb  33622  filnetlem4  33626  limsucncmpi  33690  taupilemrplb  34483  relowlssretop  34526  rdgellim  34539  matunitlindflem2  34770  ptrecube  34773  poimirlem4  34777  poimirlem17  34790  poimirlem20  34793  poimirlem23  34796  poimirlem24  34797  poimirlem26  34799  poimirlem27  34800  poimirlem29  34802  poimirlem32  34805  heicant  34808  mblfinlem1  34810  mblfinlem2  34811  mblfinlem3  34812  mblfinlem4  34813  ismblfin  34814  volsupnfl  34818  itg2addnclem  34824  itg2addnclem3  34826  itg2addnc  34827  ftc1anclem5  34852  unirep  34869  cover2  34870  indexa  34889  frinfm  34891  sdclem1  34899  fdc  34901  incsequz  34904  caushft  34917  istotbnd3  34930  0totbnd  34932  sstotbnd2  34933  sstotbnd  34934  sstotbnd3  34935  isbnd3  34943  ssbnd  34947  equivbnd  34949  prdsbnd  34952  prdstotbnd  34953  cntotbnd  34955  heibor1lem  34968  heiborlem1  34970  heiborlem3  34972  heiborlem6  34975  heiborlem8  34977  bfplem2  34982  rrncmslem  34991  iccbnd  34999  opidonOLD  35011  exidres  35037  isrngod  35057  isgrpda  35114  isdrngo2  35117  igenval  35220  igenidl  35222  prtlem10  35881  lshpnel2N  36001  lsmsat  36024  lssatomic  36027  lcvnbtwn  36041  lfl1  36086  eqlkr  36115  lshpkrlem1  36126  lshpkrex  36134  cvrcon3b  36293  cvrat4  36459  3dim3  36485  ps-2  36494  llni  36524  llnle  36534  lplni  36548  lplnle  36556  lplnexllnN  36580  lvoli  36591  lnatexN  36795  elpaddn0  36816  pclfinN  36916  lhprelat3N  37056  4atexlemex2  37087  4atex  37092  4atex2-0aOLDN  37094  4atex2-0cOLDN  37096  lautcvr  37108  cdleme0ex1N  37239  cdleme50rnlem  37560  cdleme50ex  37575  cdlemg1cex  37604  cdlemkid5  37951  cdlemk  37990  tendoex  37991  cdleml5N  37996  cdlemm10N  38134  dih1dimatlem0  38344  dihjat1lem  38444  dvh3dim2  38464  dvh3dim3N  38465  dochkr1  38494  dochkr1OLDN  38495  lcfrvalsnN  38557  lcfrlem27  38585  lcfrlem37  38595  lcfr  38601  mapd1o  38664  mapdpglem23  38710  hdmap11lem2  38858  resubeu  39085  nacsfix  39187  mzpcompact2lem  39226  eldioph  39233  diophrw  39234  diophin  39247  rexrabdioph  39269  rexzrexnn0  39279  eldioph4b  39286  rencldnfilem  39295  irrapxlem5  39301  irrapxlem6  39302  pell1234qrdich  39336  pell14qrdich  39344  infmrgelbi  39353  pellqrex  39354  pellfundre  39356  pellfundlb  39359  rmxynorm  39393  congrep  39448  acongrep  39455  jm2.27  39483  fnwe2lem2  39529  islssfgi  39550  hbtlem2  39602  hbtlem4  39604  hbtlem5  39606  dgraaub  39626  mpaaeu  39628  aaitgo  39640  rgspnval  39646  rgspncl  39647  clsk1independent  40274  elabrexg  41180  restuni3  41261  iinssd  41273  founiiun  41311  wessf1ornlem  41321  founiiun0  41327  unirnmap  41347  dstregt0  41423  uzfissfz  41470  fiminre2  41522  rpgtrecnn  41525  rexabslelem  41568  infrnmptle  41573  infxrunb3rnmpt  41578  infxrpnf  41597  supminfxr  41616  iooiinicc  41694  iooiinioc  41708  uzubioo  41719  climsuse  41765  islptre  41776  climinf3  41873  limsupmnfuzlem  41883  limsupre3lem  41889  limsupre3uzlem  41892  0cnv  41899  liminfreuzlem  41959  cnrefiisplem  41986  icccncfext  42046  cncficcgt0  42047  dvbdfbdioo  42091  ioodvbdlimc1lem1  42092  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  stoweidlem9  42171  stoweidlem14  42176  stoweidlem18  42180  stoweidlem21  42183  stoweidlem29  42191  stoweidlem34  42196  stoweidlem35  42197  stoweidlem39  42201  stoweidlem41  42203  stoweidlem45  42207  stoweidlem52  42214  stoweidlem55  42217  stoweidlem57  42219  stoweidlem60  42222  stirlinglem5  42240  stirlinglem13  42248  stirlinglem14  42249  fourierdlem16  42285  fourierdlem20  42289  fourierdlem21  42290  fourierdlem22  42291  fourierdlem25  42294  fourierdlem31  42300  fourierdlem39  42308  fourierdlem41  42310  fourierdlem42  42311  fourierdlem47  42315  fourierdlem48  42316  fourierdlem49  42317  fourierdlem51  42319  fourierdlem63  42331  fourierdlem64  42332  fourierdlem65  42333  fourierdlem77  42345  fourierdlem81  42349  fourierdlem83  42351  fourierdlem103  42371  fourierdlem104  42372  elaa2lem  42395  etransclem47  42443  qndenserrnbl  42457  ioorrnopnlem  42466  ioorrnopnxrlem  42468  intsaluni  42489  salgencntex  42503  subsaliuncllem  42517  sge0resplit  42565  sge0seq  42605  sge0reuz  42606  nnfoctbdjlem  42614  meaiininclem  42645  hoicvrrex  42715  ovnlecvr  42717  ovnlerp  42721  hoidmv1lelem2  42751  hoidmvlelem2  42755  hoidmvlelem3  42756  ovnhoilem1  42760  ovnlecvr2  42769  hoiqssbl  42784  ovolval4lem2  42809  ovolval5lem2  42812  ovnovollem1  42815  ovnovollem2  42816  iinhoiicclem  42832  smfinflem  42968  smflimsuplem7  42977  sprsymrelfolem2  43532  perfectALTV  43765  9gbo  43816  11gbo  43817  nnsum3primes4  43830  nnsum3primesprm  43832  ssnn0ssfz  44325  lincsumcl  44414  lincscmcl  44415  zlmodzxzldep  44487  ldepsnlinc  44491  line2ylem  44666  line2xlem  44668  aacllem  44830
  Copyright terms: Public domain W3C validator