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

Theorem rspcev 3498
Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspcev ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcev
StepHypRef Expression
1 nfv 2005 . 2 𝑥𝜓
2 rspcv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2rspce 3493 1 ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2155  wrex 3093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-rex 3098  df-v 3389
This theorem is referenced by:  rspceaimv  3506  rspc2ev  3513  rspc3ev  3515  rspceeqv  3516  reu6i  3589  rspesbca  3709  eliuni  4711  brralrspcev  4897  wefrc  5299  wereu2  5302  xpdifid  5767  onfr  5970  ordunidif  5980  eliman0  6437  dffv2  6486  elrnrexdm  6579  eldmrexrn  6581  elabrex  6719  f1elima  6738  fliftfun  6780  fliftval  6784  f1oiso2  6820  sorpssuni  7170  sorpssint  7171  onssmin  7221  onminex  7231  tfrlem12  7715  seqomlem2  7776  oawordeulem  7865  oaass  7872  odi  7890  omass  7891  omeulem1  7893  oen0  7897  oelim2  7906  oeeulem  7912  nnawordex  7948  boxcutc  8182  snfi  8271  onfin  8384  pssnn  8411  ssnnfi  8412  dif1en  8426  findcard  8432  frfi  8438  fisupg  8441  nnsdomg  8452  unfi  8460  fissuni  8504  fipreima  8505  finsschain  8506  indexfi  8507  marypha1lem  8572  eqsup  8595  supmax  8606  fisup2g  8607  fisupcl  8608  supisoex  8613  infmin  8633  fiinfg  8638  fiinf2g  8639  wofib  8683  wemaplem2  8685  card2inf  8693  brwdom2  8711  cnfcom3clem  8843  trcl  8845  r1ordg  8882  r1pwss  8888  tz9.12lem3  8893  tz9.12  8894  r1elwf  8900  tcrank  8988  scottex  8989  scott0  8990  isnumi  9049  onsdom  9099  ondomen  9137  infpwfien  9162  cardaleph  9189  infenaleph  9191  alephfplem4  9207  alephfp2  9209  dfac2b  9230  dfac2OLD  9232  ackbij1lem18  9338  ackbij1  9339  cflem  9347  cflecard  9354  cfsuc  9358  cfflb  9360  cofsmo  9370  coftr  9374  fin23lem7  9417  fin23lem11  9418  enfin2i  9422  fin23lem26  9426  isf32lem5  9458  isf34lem4  9478  isfin1-3  9487  fin1a2lem7  9507  axdc3lem4  9554  ttukeylem7  9616  iunfo  9640  ficard  9666  pwcfsdom  9684  fpwwe2lem12  9742  wunex  9840  eltsk2g  9852  grur1  9921  axgroth6  9929  inaprc  9937  nqereu  10030  archnq  10081  genpnmax  10108  ltexpri  10144  prlem936  10148  recexpr  10152  supexpr  10155  negexsr  10202  recexsrlem  10203  recexsr  10207  supsrlem  10211  axrnegex  10262  axrrecex  10263  axpre-sup  10269  1re  10319  dedekind  10479  dedekindle  10480  cnegex  10496  cnegex2  10497  recex  10938  receu  10951  cju  11295  nn2ge  11325  nominpos  11530  zdiv  11707  btwnz  11739  uzwo  11964  ublbneg  11986  lbzbi  11989  zsupss  11990  uzsupss  11993  rpnnen1lem1  12028  rpnnen1lem3  12029  rpnnen1lem4  12030  rpnnen1lem5  12031  z2ge  12241  qbtwnre  12242  qbtwnxr  12243  xralrple  12248  xrsupsslem  12349  xrinfmsslem  12350  supxrpnf  12360  icc0  12435  uzsup  12880  expnbnd  13210  expmulnbnd  13213  hashkf  13333  hashdom  13380  iswrdi  13514  rtrclreclem1  14015  rtrclreclem2  14016  rtrclreclem3  14017  01sqrex  14207  resqrex  14208  sqrtneg  14225  abs1m  14292  rexanuz  14302  rexuz3  14305  rexuzre  14309  sqreu  14317  o1lo1  14485  climconst  14491  rlimclim1  14493  climshftlem  14522  rlimo1  14564  lo1add  14574  lo1mul  14575  lo1le  14599  isercoll  14615  serf0  14628  zsum  14666  fsum  14668  fsumcvg3  14677  mertenslem1  14831  ntrivcvgn0  14845  ntrivcvgmullem  14848  zprod  14882  fprod  14886  fprodntriv  14887  dvdsval2  15200  dvds0lem  15209  dvds1lem  15210  dvds2lem  15211  odd2np1lem  15278  odd2np1  15279  opeo  15303  omeo  15304  divalglem9  15338  gcdcllem3  15436  lcmcllem  15522  qredeu  15584  exprmfct  15627  isprm5  15630  odzcllem  15708  reumodprminv  15720  modprm0  15721  nnnn0modprm0  15722  pythagtriplem19  15749  pcprmpw2  15797  pockthi  15822  infpnlem2  15826  vdwlem2  15897  vdwlem10  15905  vdwlem13  15908  ramub1lem1  15941  cshwrepswhash1  16015  imasleval  16400  mreexexlem3d  16505  mreexexlem4d  16506  iscatd  16532  poslubd  17347  fpwipodrs  17363  ismgmid2  17466  mgmidsssn0  17468  gsumval2a  17478  ismndd  17512  isgrpd2  17641  isgrpd  17643  imasgrp2  17729  mhmmnd  17736  ghmgrp  17738  gaorber  17936  orbsta  17941  cayleyth  18030  pmtrdifel  18095  pmtrdifwrdel  18100  pmtrdifwrdel2  18101  psgnunilem2  18110  psgnunilem3  18111  psgnvalii  18124  pgpfi1  18205  sylow1lem3  18210  sylow1lem5  18212  pgpfi  18215  sylow2alem2  18228  efgredeu  18360  lt6abl  18491  pgpfac1lem3a  18671  pgpfac1lem3  18672  pgpfac1lem5  18674  pgpfaclem1  18676  pgpfaclem3  18678  ablfaclem2  18681  dvdsrmul  18844  dvdsr01  18851  irredrmul  18903  lspf  19175  lspval  19176  lssats2  19201  lspfixed  19329  lspfixedOLD  19330  lspsolvlem  19344  aspval  19531  evlseu  19718  zringlpir  20039  zncyg  20098  cygth  20121  frlmup4  20344  fiinbas  20964  topbas  20984  pptbas  21020  clsval  21049  elcls  21085  neiint  21116  neips  21125  opnneissb  21126  opnssneib  21127  innei  21137  neiptopnei  21144  restbas  21170  neitr  21192  pnfnei  21232  mnfnei  21233  lmconst  21273  iscnp4  21275  cncnpi  21290  cnconst2  21295  cnprest  21301  cnpdis  21305  nrmsep  21369  regsep2  21388  cmpcovf  21402  cmpsub  21411  cmpcld  21413  hauscmplem  21417  conncompid  21442  2ndci  21459  2ndcsb  21460  2ndc1stc  21462  1stcrest  21464  2ndcctbss  21466  2ndcdisj  21467  2ndcomap  21469  2ndcsep  21470  dis2ndc  21471  restlly  21494  islly2  21495  hausllycmp  21505  cldllycmp  21506  lly1stc  21507  dislly  21508  ssref  21523  refref  21524  finlocfin  21531  dissnlocfin  21540  locfindis  21541  llycmpkgen2  21561  cmpkgen  21562  1stckgenlem  21564  elptr  21584  ptbasfi  21592  neitx  21618  ptpjopn  21623  txcnp  21631  ptcnplem  21632  txlly  21647  txnlly  21648  txtube  21651  txcmplem1  21652  tx1stc  21661  txkgen  21663  xkococnlem  21670  txconn  21700  tgqtop  21723  kqreglem1  21752  kqreglem2  21753  kqnrmlem1  21754  kqnrmlem2  21755  reghmph  21804  nrmhmph  21805  fbssfi  21848  opnfbas  21853  isfil2  21867  fsubbas  21878  ssfg  21883  fgss2  21885  fbasrn  21895  filuni  21896  fgtr  21901  ssufl  21929  uffix  21932  elfm2  21959  elfm3  21961  imaelfm  21962  rnelfmlem  21963  rnelfm  21964  fmfnfmlem4  21968  fmfnfm  21969  fmco  21972  ufldom  21973  hausflim  21992  flimcls  21996  hauspwpwf1  21998  flffbas  22006  txflf  22017  fclscf  22036  fclsfnflim  22038  alexsubALTlem4  22061  alexsubALT  22062  tmdgsum2  22107  symgtgp  22112  subgntr  22117  opnsubg  22118  ghmcnp  22125  qustgpopn  22130  tsmsfbas  22138  tsmsxplem1  22163  ustexsym  22226  elrnust  22235  trust  22240  utoptop  22245  restutop  22248  restutopopn  22249  ustuqtop4  22255  utopsnneiplem  22258  iducn  22294  fmucnd  22303  cfilufg  22304  trcfilu  22305  neipcfilu  22307  imasdsf1olem  22385  blssps  22436  blss  22437  blssexps  22438  blssex  22439  ssblex  22440  blin2  22441  neibl  22513  blcld  22517  metss2  22524  stdbdmopn  22530  met1stc  22533  met2ndci  22534  metrest  22536  prdsxmslem2  22541  metcnp3  22552  metuval  22561  metustexhalf  22568  metustfbas  22569  cfilucfil  22571  restmetu  22582  dscopn  22585  ngptgp  22647  nlmvscnlem1  22697  tgioo  22806  tgqioo  22810  xrsmopn  22822  zcld  22823  recld2  22824  zdis  22826  icccmplem1  22832  icccmplem2  22833  xmetdcn2  22847  addcnlem  22874  xrhmeo  22952  cnheibor  22961  cnllycmp  22962  lebnumlem3  22969  lebnum  22970  xlebnum  22971  lebnumii  22972  elpi1i  23052  ipcnlem1  23250  lmnn  23267  iscfil3  23277  cfilres  23300  flimcfil  23318  bcthlem4  23330  bcthlem5  23331  minveclem4c  23402  minveclem2  23403  minveclem3b  23405  minveclem3  23406  minveclem4  23409  minveclem6  23411  ivthlem2  23427  ivth  23429  ivthle  23431  ivthle2  23432  elovolmr  23451  ovolunlem1  23472  ovoliunlem2  23478  ovolicc1  23491  iundisj  23523  iunmbl2  23532  dyadmbllem  23574  volivth  23582  mbflimsup  23641  i1faddlem  23668  i1fmullem  23669  itg2lr  23705  itg2monolem1  23725  limcnlp  23850  ellimc3  23851  limcflf  23853  limciun  23866  rollelem  23960  c1lip1  23968  lhop1lem  23984  ply1divex  24104  ig1peu  24139  elply2  24160  coeeq  24191  plydivlem3  24258  plydivlem4  24259  elqaalem3  24284  qaa  24286  iaa  24288  aareccl  24289  aannenlem2  24292  aalioulem2  24296  aalioulem3  24297  aalioulem5  24299  aalioulem6  24300  aaliou  24301  aaliou2  24303  aaliou3lem8  24308  ulmshftlem  24351  reeff1o  24409  pilem2  24414  pilem3  24415  pilem3OLD  24416  efif1olem2  24498  efopn  24612  cxpcn3lem  24696  cxpeq  24706  dcubic2  24779  quart  24796  xrlimcnp  24903  ftalem5  25011  ftalem7  25013  sgmnncl  25081  dvdsppwf1o  25120  musum  25125  perfect  25164  dchrptlem1  25197  dchrptlem2  25198  dchrpt  25200  bpos1lem  25215  lgsqrlem4  25282  lgsdchrval  25287  2sqblem  25364  dchrisumlem3  25388  chpdifbndlem2  25451  pntrsumbnd2  25464  pntpbnd1  25483  pntpbnd2  25484  pntpbnd  25485  pntibndlem2  25488  pntibndlem3  25489  pntleme  25505  pntlem3  25506  axtgcont  25576  tgcgrxfr  25621  legid  25690  btwnleg  25691  leg0  25695  tghilberti1  25740  tglnpt2  25744  colline  25752  mirreu3  25757  isperp2  25818  colperpex  25833  opphllem4  25850  lnopp2hpgb  25863  hpgerlem  25865  lmiopp  25902  brbtwn  25987  brcgr  25988  brbtwn2  25993  axpasch  26029  axlowdimlem14  26043  axlowdim2  26048  axcontlem2  26053  axcontlem4  26055  axcontlem8  26059  axcontlem10  26061  axcontlem12  26063  fusgrn0degnn0  26617  clwlkclwwlkf  27145  friendshipgt3  27580  lpni  27657  isgrpoi  27675  vacn  27871  smcnlem  27874  nmosetn0  27942  nmoolb  27948  nmobndi  27952  nmoo0  27968  nmlno0lem  27970  isblo3i  27978  blo3i  27979  blocnilem  27981  ubthlem1  28048  minvecolem2  28053  minvecolem3  28054  minvecolem4c  28057  minvecolem4  28058  minvecolem5  28059  minvecolem6  28060  norm1exi  28429  occl  28485  spanval  28514  spancl  28517  shsval2i  28568  ococin  28589  pjoml6i  28770  nmopsetn0  29046  nmfnsetn0  29059  nmoplb  29088  nmfnlb  29105  nmop0  29167  nmfn0  29168  nmlnop0iALT  29176  nmopun  29195  nmcexi  29207  lnconi  29214  lnopcnbd  29217  lnfncnbd  29238  riesz3i  29243  riesz1  29246  cnlnadjlem2  29249  cnlnadjlem8  29255  cnlnadjlem9  29256  adjbd1o  29266  branmfn  29286  opsqrlem1  29321  pjnmopi  29329  strlem1  29431  stri  29438  hstri  29446  cvcon3  29465  cvnbtwn  29467  superpos  29535  shatomici  29539  atcvat4i  29578  mdsymlem2  29585  cdj1i  29614  cdj3i  29622  rexunirn  29651  foresf1o  29662  iundisjf  29721  elunirn2  29772  aciunf1lem  29783  fgreu  29792  fcnvgreu  29793  xrge0infss  29846  ssnnssfz  29870  iundisjfi  29876  xreceu  29949  rexdiv  29953  isarchi3  30060  archirngz  30062  archiabllem2a  30067  rhmdvdsr  30137  fimaproj  30219  qtophaus  30222  reff  30225  locfinreflem  30226  cmpcref  30236  dispcmp  30245  metidval  30252  pstmval  30257  tpr2rico  30277  pnfneige0  30316  qqhucn  30355  rrhre  30384  indf1ofs  30407  esumcst  30444  esumpcvgval  30459  dmsigagen  30526  rossros  30562  dya2icoseg  30658  dya2iocnrect  30662  dya2iocuni  30664  eulerpartlemgvv  30757  dstfrvunirn  30855  ballotlem4  30879  ballotlemic  30887  ballotlem1c  30888  ballotlemrc  30911  signsw0g  30952  signswmnd  30953  prodfzo03  31000  tgoldbachgt  31060  subfacp1lem3  31481  erdsze2lem2  31503  cnpconn  31529  txpconn  31531  ptpconn  31532  indispconn  31533  connpconn  31534  cvxpconn  31541  cnllysconn  31544  cvmsss2  31573  cvmcov2  31574  cvmopnlem  31577  cvmliftlem14  31596  cvmliftlem15  31597  cvmlift2lem11  31612  cvmlift2lem12  31613  cvmlift2lem13  31614  cvmlift3lem2  31619  cvmlift3lem6  31623  cvmlift3lem9  31626  mthmi  31791  br8  31962  br6  31963  br4  31964  dfon2lem9  32010  trpredtr  32044  dftrpred3g  32047  frpomin  32053  frmin  32057  poseq  32068  wzel  32084  wsuclem  32085  wsuclb  32088  frrlem5e  32103  elno2  32122  sltval2  32124  noreson  32128  sltres  32130  noseponlem  32132  nolesgn2o  32139  nodense  32157  nosupfv  32167  nosupres  32168  nosupbnd1lem3  32171  nosupbnd1lem5  32173  nosupbnd2lem1  32176  noetalem3  32180  noetalem5  32182  imagesset  32375  fvtransport  32454  brcolinear  32481  brsegle  32530  seglerflx  32534  seglemin  32535  btwnsegle  32539  fvray  32563  fvline  32566  hilbert1.1  32576  elhf2  32597  0hf  32599  nn0prpwlem  32632  nn0prpw  32633  fness  32659  fneref  32660  fnessref  32667  refssfne  32668  neibastop2lem  32670  fnemeet1  32676  tailfb  32687  filnetlem4  32691  limsucncmpi  32755  taupilemrplb  33477  relowlssretop  33521  matunitlindflem2  33713  ptrecube  33716  poimirlem4  33720  poimirlem17  33733  poimirlem20  33736  poimirlem23  33739  poimirlem24  33740  poimirlem26  33742  poimirlem27  33743  poimirlem29  33745  poimirlem32  33748  heicant  33751  mblfinlem1  33753  mblfinlem2  33754  mblfinlem3  33755  mblfinlem4  33756  ismblfin  33757  volsupnfl  33761  itg2addnclem  33767  itg2addnclem3  33769  itg2addnc  33770  ftc1anclem5  33795  unirep  33813  cover2  33814  indexa  33834  frinfm  33836  sdclem1  33844  fdc  33846  incsequz  33849  caushft  33862  istotbnd3  33875  0totbnd  33877  sstotbnd2  33878  sstotbnd  33879  sstotbnd3  33880  isbnd3  33888  ssbnd  33892  equivbnd  33894  prdsbnd  33897  prdstotbnd  33898  cntotbnd  33900  heibor1lem  33913  heiborlem1  33915  heiborlem3  33917  heiborlem6  33920  heiborlem8  33922  bfplem2  33927  rrncmslem  33936  iccbnd  33944  opidonOLD  33956  exidres  33982  isrngod  34002  isgrpda  34059  isdrngo2  34062  igenval  34165  igenidl  34167  prtlem10  34638  lshpnel2N  34759  lsmsat  34782  lssatomic  34785  lcvnbtwn  34799  lfl1  34844  eqlkr  34873  lshpkrlem1  34884  lshpkrex  34892  cvrcon3b  35051  cvrat4  35217  3dim3  35243  ps-2  35252  llni  35282  llnle  35292  lplni  35306  lplnle  35314  lplnexllnN  35338  lvoli  35349  lnatexN  35553  elpaddn0  35574  pclfinN  35674  lhprelat3N  35814  4atexlemex2  35845  4atex  35850  4atex2-0aOLDN  35852  4atex2-0cOLDN  35854  lautcvr  35866  cdleme0ex1N  35998  cdleme50rnlem  36319  cdleme50ex  36334  cdlemg1cex  36363  cdlemkid5  36710  cdlemk  36749  tendoex  36750  cdleml5N  36755  cdlemm10N  36893  dih1dimatlem0  37103  dihjat1lem  37203  dvh3dim2  37223  dvh3dim3N  37224  dochkr1  37253  dochkr1OLDN  37254  lcfrvalsnN  37316  lcfrlem27  37344  lcfrlem37  37354  lcfr  37360  mapd1o  37423  mapdpglem23  37469  hdmap11lem2  37617  nacsfix  37771  mzpcompact2lem  37810  eldioph  37817  diophrw  37818  diophin  37832  rexrabdioph  37854  rexzrexnn0  37864  eldioph4b  37871  rencldnfilem  37880  irrapxlem5  37886  irrapxlem6  37887  pell1234qrdich  37921  pell14qrdich  37929  infmrgelbi  37938  pellqrex  37939  pellfundre  37941  pellfundlb  37944  rmxynorm  37978  congrep  38035  acongrep  38042  jm2.27  38070  fnwe2lem2  38116  islssfgi  38137  hbtlem2  38189  hbtlem4  38191  hbtlem5  38193  dgraaub  38213  mpaaeu  38215  aaitgo  38227  rgspnval  38233  rgspncl  38234  clsk1independent  38838  elabrexg  39694  restuni3  39787  iinssd  39799  founiiun  39843  founiiun0  39860  unirnmap  39881  dstregt0  39969  uzfissfz  40016  fiminre2  40068  rpgtrecnn  40071  rexabslelem  40118  infrnmptle  40123  infxrunb3rnmpt  40128  infxrpnf  40147  supminfxr  40167  iooiinicc  40243  iooiinioc  40257  uzubioo  40268  climsuse  40314  islptre  40325  climinf3  40422  limsupmnfuzlem  40432  limsupre3lem  40438  limsupre3uzlem  40441  0cnv  40448  liminfreuzlem  40508  cnrefiisplem  40529  icccncfext  40574  cncficcgt0  40575  dvbdfbdioo  40619  ioodvbdlimc1lem1  40620  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  stoweidlem9  40699  stoweidlem14  40704  stoweidlem18  40708  stoweidlem21  40711  stoweidlem29  40719  stoweidlem34  40724  stoweidlem35  40725  stoweidlem39  40729  stoweidlem41  40731  stoweidlem45  40735  stoweidlem52  40742  stoweidlem55  40745  stoweidlem57  40747  stoweidlem60  40750  stirlinglem5  40768  stirlinglem13  40776  stirlinglem14  40777  fourierdlem16  40813  fourierdlem20  40817  fourierdlem21  40818  fourierdlem22  40819  fourierdlem25  40822  fourierdlem31  40828  fourierdlem39  40836  fourierdlem41  40838  fourierdlem42  40839  fourierdlem47  40843  fourierdlem48  40844  fourierdlem49  40845  fourierdlem51  40847  fourierdlem63  40859  fourierdlem64  40860  fourierdlem65  40861  fourierdlem77  40873  fourierdlem81  40877  fourierdlem83  40879  fourierdlem103  40899  fourierdlem104  40900  elaa2lem  40923  etransclem47  40971  qndenserrnbl  40988  ioorrnopnlem  40997  ioorrnopnxrlem  40999  intsaluni  41020  salgencntex  41034  subsaliuncllem  41048  sge0resplit  41096  sge0seq  41136  sge0reuz  41137  nnfoctbdjlem  41145  meaiininclem  41176  hoicvrrex  41246  ovnlecvr  41248  ovnlerp  41252  hoidmv1lelem2  41282  hoidmvlelem2  41286  hoidmvlelem3  41287  ovnhoilem1  41291  ovnlecvr2  41300  hoiqssbl  41315  ovolval4lem2  41340  ovolval5lem2  41343  ovnovollem1  41346  ovnovollem2  41347  iinhoiicclem  41363  smfinflem  41499  smflimsuplem7  41508  perfectALTV  42201  9gbo  42231  11gbo  42232  nnsum3primes4  42245  nnsum3primesprm  42247  sprsymrelfolem2  42305  ssnn0ssfz  42689  lincsumcl  42782  lincscmcl  42783  zlmodzxzldep  42855  ldepsnlinc  42859  aacllem  43112
  Copyright terms: Public domain W3C validator