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

Theorem rspcev 3622
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 3615 . 2 (𝐴𝐵 → (𝜓 → ∃𝑥𝐵 𝜑))
54imp 407 1 ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wrex 3139
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144
This theorem is referenced by:  rspceaimv  3627  rspc2ev  3634  rspc3ev  3636  rspceeqv  3637  reu6i  3718  rspesbca  3863  eliuni  4918  brralrspcev  5118  wefrc  5543  wereu2  5546  xpdifid  6019  onfr  6224  ordunidif  6233  eliman0  6699  dffv2  6750  elrnrexdm  6848  eldmrexrn  6850  elabrex  6993  f1elima  7012  fliftfun  7054  fliftval  7058  f1oiso2  7094  sorpssuni  7447  sorpssint  7448  onssmin  7500  onminex  7510  fimaproj  7820  tfrlem12  8016  seqomlem2  8078  oawordeulem  8170  oaass  8177  odi  8195  omass  8196  omeulem1  8198  oen0  8202  oelim2  8211  oeeulem  8217  nnawordex  8253  boxcutc  8494  snfi  8583  onfin  8698  pssnn  8725  ssnnfi  8726  dif1en  8740  findcard  8746  frfi  8752  fisupg  8755  nnsdomg  8766  unfi  8774  fissuni  8818  fipreima  8819  finsschain  8820  indexfi  8821  marypha1lem  8886  eqsup  8909  supmax  8920  fisup2g  8921  fisupcl  8922  supisoex  8927  infmin  8947  fiinfg  8952  fiinf2g  8953  wofib  8998  wemaplem2  9000  card2inf  9008  brwdom2  9026  cnfcom3clem  9157  trcl  9159  r1ordg  9196  r1pwss  9202  tz9.12lem3  9207  tz9.12  9208  r1elwf  9214  tcrank  9302  scottex  9303  scott0  9304  isnumi  9364  onsdom  9414  ondomen  9452  infpwfien  9477  cardaleph  9504  infenaleph  9506  alephfplem4  9522  alephfp2  9524  dfac2b  9545  ackbij1lem18  9648  ackbij1  9649  cflem  9657  cflecard  9664  cfsuc  9668  cfflb  9670  cofsmo  9680  coftr  9684  fin23lem7  9727  fin23lem11  9728  enfin2i  9732  fin23lem26  9736  isf32lem5  9768  isf34lem4  9788  isfin1-3  9797  fin1a2lem7  9817  axdc3lem4  9864  ttukeylem7  9926  iunfo  9950  ficard  9976  pwcfsdom  9994  fpwwe2lem12  10052  wunex  10150  eltsk2g  10162  grur1  10231  axgroth6  10239  inaprc  10247  nqereu  10340  archnq  10391  genpnmax  10418  ltexpri  10454  prlem936  10458  recexpr  10462  supexpr  10465  negexsr  10513  recexsrlem  10514  recexsr  10518  supsrlem  10522  axrnegex  10573  axrrecex  10574  axpre-sup  10580  1re  10630  dedekind  10792  dedekindle  10793  cnegex  10810  cnegex2  10811  recex  11261  receu  11274  cju  11623  nn2ge  11653  nominpos  11863  zdiv  12041  btwnz  12073  uzwo  12300  ublbneg  12322  lbzbi  12325  zsupss  12326  uzsupss  12329  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem4  12369  rpnnen1lem5  12370  z2ge  12581  qbtwnre  12582  qbtwnxr  12583  xralrple  12588  xrsupsslem  12690  xrinfmsslem  12691  supxrpnf  12701  icc0  12776  uzsup  13221  expnbnd  13583  expmulnbnd  13586  hashkf  13682  hashdom  13730  iswrdi  13855  rtrclreclem1  14407  rtrclreclem2  14408  rtrclreclem3  14409  01sqrex  14599  resqrex  14600  sqrtneg  14617  abs1m  14685  rexanuz  14695  rexuz3  14698  rexuzre  14702  sqreu  14710  o1lo1  14884  climconst  14890  rlimclim1  14892  climshftlem  14921  rlimo1  14963  lo1add  14973  lo1mul  14974  lo1le  14998  isercoll  15014  serf0  15027  zsum  15065  fsum  15067  fsumcvg3  15076  mertenslem1  15230  ntrivcvgn0  15244  ntrivcvgmullem  15247  zprod  15281  fprod  15285  fprodntriv  15286  dvdsval2  15600  dvds0lem  15610  dvds1lem  15611  dvds2lem  15612  odd2np1lem  15679  odd2np1  15680  opeo  15704  omeo  15705  divalglem9  15742  gcdcllem3  15840  lcmcllem  15930  qredeu  15992  exprmfct  16038  isprm5  16041  odzcllem  16119  reumodprminv  16131  modprm0  16132  nnnn0modprm0  16133  pythagtriplem19  16160  pcprmpw2  16208  pockthi  16233  infpnlem2  16237  vdwlem2  16308  vdwlem10  16316  vdwlem13  16319  ramub1lem1  16352  cshwrepswhash1  16426  imasleval  16804  mreexexlem3d  16907  mreexexlem4d  16908  iscatd  16934  poslubd  17748  fpwipodrs  17764  ismgmid2  17868  mgmidsssn0  17872  gsumval2a  17885  ismndd  17923  isgrpd2  18063  isgrpd  18065  imasgrp2  18154  mhmmnd  18161  ghmgrp  18163  gaorber  18378  orbsta  18383  cayleyth  18474  pmtrdifel  18539  pmtrdifwrdel  18544  pmtrdifwrdel2  18545  psgnunilem2  18554  psgnunilem3  18555  psgnvalii  18568  pgpfi1  18651  sylow1lem3  18656  sylow1lem5  18658  pgpfi  18661  sylow2alem2  18674  efgredeu  18809  lt6abl  18946  pgpfac1lem3a  19129  pgpfac1lem3  19130  pgpfac1lem5  19132  pgpfaclem1  19134  pgpfaclem3  19136  ablfaclem2  19139  dvdsrmul  19329  dvdsr01  19336  irredrmul  19388  lspf  19677  lspval  19678  lssats2  19703  lspfixed  19831  lspsolvlem  19845  aspval  20032  evlseu  20226  zringlpir  20566  zncyg  20625  cygth  20648  frlmup4  20875  fiinbas  21490  topbas  21510  pptbas  21546  clsval  21575  elcls  21611  neiint  21642  neips  21651  opnneissb  21652  opnssneib  21653  innei  21663  neiptopnei  21670  restbas  21696  neitr  21718  pnfnei  21758  mnfnei  21759  lmconst  21799  iscnp4  21801  cncnpi  21816  cnconst2  21821  cnprest  21827  cnpdis  21831  nrmsep  21895  regsep2  21914  cmpcovf  21929  cmpsub  21938  cmpcld  21940  hauscmplem  21944  conncompid  21969  2ndci  21986  2ndcsb  21987  2ndc1stc  21989  1stcrest  21991  2ndcctbss  21993  2ndcdisj  21994  2ndcomap  21996  2ndcsep  21997  dis2ndc  21998  restlly  22021  islly2  22022  hausllycmp  22032  cldllycmp  22033  lly1stc  22034  dislly  22035  ssref  22050  refref  22051  finlocfin  22058  dissnlocfin  22067  locfindis  22068  llycmpkgen2  22088  cmpkgen  22089  1stckgenlem  22091  elptr  22111  ptbasfi  22119  neitx  22145  ptpjopn  22150  txcnp  22158  ptcnplem  22159  txlly  22174  txnlly  22175  txtube  22178  txcmplem1  22179  tx1stc  22188  txkgen  22190  xkococnlem  22197  txconn  22227  tgqtop  22250  kqreglem1  22279  kqreglem2  22280  kqnrmlem1  22281  kqnrmlem2  22282  reghmph  22331  nrmhmph  22332  fbssfi  22375  opnfbas  22380  isfil2  22394  fsubbas  22405  ssfg  22410  fgss2  22412  fbasrn  22422  filuni  22423  fgtr  22428  ssufl  22456  uffix  22459  elfm2  22486  elfm3  22488  imaelfm  22489  rnelfmlem  22490  rnelfm  22491  fmfnfmlem4  22495  fmfnfm  22496  fmco  22499  ufldom  22500  hausflim  22519  flimcls  22523  hauspwpwf1  22525  flffbas  22533  txflf  22544  fclscf  22563  fclsfnflim  22565  alexsubALTlem4  22588  alexsubALT  22589  tmdgsum2  22634  symgtgp  22639  subgntr  22644  opnsubg  22645  ghmcnp  22652  qustgpopn  22657  tsmsfbas  22665  tsmsxplem1  22690  ustexsym  22753  elrnust  22762  trust  22767  utoptop  22772  restutop  22775  restutopopn  22776  ustuqtop4  22782  utopsnneiplem  22785  iducn  22821  fmucnd  22830  cfilufg  22831  trcfilu  22832  neipcfilu  22834  imasdsf1olem  22912  blssps  22963  blss  22964  blssexps  22965  blssex  22966  ssblex  22967  blin2  22968  neibl  23040  blcld  23044  metss2  23051  stdbdmopn  23057  met1stc  23060  met2ndci  23061  metrest  23063  prdsxmslem2  23068  metcnp3  23079  metuval  23088  metustexhalf  23095  metustfbas  23096  cfilucfil  23098  restmetu  23109  dscopn  23112  ngptgp  23174  nlmvscnlem1  23224  tgioo  23333  tgqioo  23337  xrsmopn  23349  zcld  23350  recld2  23351  zdis  23353  icccmplem1  23359  icccmplem2  23360  xmetdcn2  23374  addcnlem  23401  xrhmeo  23479  cnheibor  23488  cnllycmp  23489  lebnumlem3  23496  lebnum  23497  xlebnum  23498  lebnumii  23499  elpi1i  23579  ipcnlem1  23777  lmnn  23795  iscfil3  23805  cfilres  23828  flimcfil  23846  bcthlem4  23859  bcthlem5  23860  minveclem4c  23957  minveclem2  23958  minveclem3b  23960  minveclem3  23961  minveclem4  23964  minveclem6  23966  ivthlem2  23982  ivth  23984  ivthle  23986  ivthle2  23987  elovolmr  24006  ovolunlem1  24027  ovoliunlem2  24033  ovolicc1  24046  iundisj  24078  iunmbl2  24087  dyadmbllem  24129  volivth  24137  mbflimsup  24196  i1faddlem  24223  i1fmullem  24224  itg2lr  24260  itg2monolem1  24280  limcnlp  24405  ellimc3  24406  limcflf  24408  limciun  24421  rollelem  24515  c1lip1  24523  lhop1lem  24539  ply1divex  24659  ig1peu  24694  elply2  24715  coeeq  24746  plydivlem3  24813  plydivlem4  24814  elqaalem3  24839  qaa  24841  iaa  24843  aareccl  24844  aannenlem2  24847  aalioulem2  24851  aalioulem3  24852  aalioulem5  24854  aalioulem6  24855  aaliou  24856  aaliou2  24858  aaliou3lem8  24863  ulmshftlem  24906  reeff1o  24964  pilem2  24969  pilem3  24970  efif1olem2  25054  efopn  25168  cxpcn3lem  25255  cxpeq  25265  dcubic2  25349  quart  25366  xrlimcnp  25474  ftalem5  25582  ftalem7  25584  sgmnncl  25652  dvdsppwf1o  25691  musum  25696  perfect  25735  dchrptlem1  25768  dchrptlem2  25769  dchrpt  25771  bpos1lem  25786  lgsqrlem4  25853  lgsdchrval  25858  2sqblem  25935  dchrisumlem3  25995  chpdifbndlem2  26058  pntrsumbnd2  26071  pntpbnd1  26090  pntpbnd2  26091  pntpbnd  26092  pntibndlem2  26095  pntibndlem3  26096  pntleme  26112  pntlem3  26113  axtgcont  26183  tgcgrxfr  26232  legid  26301  btwnleg  26302  leg0  26306  tghilberti1  26351  tglnpt2  26355  colline  26363  mirreu3  26368  isperp2  26429  colperpex  26447  lnopp2hpgb  26477  hpgerlem  26479  brbtwn  26613  brcgr  26614  brbtwn2  26619  axpasch  26655  axlowdimlem14  26669  axlowdim2  26674  axcontlem2  26679  axcontlem4  26681  axcontlem8  26685  axcontlem10  26687  axcontlem12  26689  fusgrn0degnn0  27209  friendshipgt3  28105  lpni  28185  isgrpoi  28203  vacn  28399  smcnlem  28402  nmosetn0  28470  nmoolb  28476  nmobndi  28480  nmoo0  28496  nmlno0lem  28498  isblo3i  28506  blo3i  28507  blocnilem  28509  ubthlem1  28575  minvecolem2  28580  minvecolem3  28581  minvecolem4c  28584  minvecolem4  28585  minvecolem5  28586  minvecolem6  28587  norm1exi  28955  occl  29009  spanval  29038  spancl  29041  shsval2i  29092  ococin  29113  pjoml6i  29294  nmopsetn0  29570  nmfnsetn0  29583  nmoplb  29612  nmfnlb  29629  nmop0  29691  nmfn0  29692  nmlnop0iALT  29700  nmopun  29719  nmcexi  29731  lnconi  29738  lnopcnbd  29741  lnfncnbd  29762  riesz3i  29767  riesz1  29770  cnlnadjlem2  29773  cnlnadjlem8  29779  cnlnadjlem9  29780  adjbd1o  29790  branmfn  29810  opsqrlem1  29845  pjnmopi  29853  strlem1  29955  stri  29962  hstri  29970  cvcon3  29989  cvnbtwn  29991  superpos  30059  shatomici  30063  atcvat4i  30102  mdsymlem2  30109  cdj1i  30138  cdj3i  30146  rexunirn  30184  foresf1o  30193  iundisjf  30268  elunirn2  30325  aciunf1lem  30336  fnpreimac  30345  fgreu  30346  fcnvgreu  30347  xrge0infss  30411  ssnnssfz  30437  iundisjfi  30446  xreceu  30526  rexdiv  30530  isarchi3  30744  archirngz  30746  archiabllem2a  30751  rhmdvdsr  30819  0nellinds  30863  qtophaus  31000  reff  31003  locfinreflem  31004  cmpcref  31014  dispcmp  31023  metidval  31030  pstmval  31035  tpr2rico  31055  pnfneige0  31094  qqhucn  31133  rrhre  31162  indf1ofs  31185  esumcst  31222  esumpcvgval  31237  dmsigagen  31303  rossros  31339  dya2icoseg  31435  dya2iocnrect  31439  dya2iocuni  31441  eulerpartlemgvv  31534  dstfrvunirn  31632  ballotlem4  31656  ballotlemic  31664  ballotlem1c  31665  ballotlemrc  31688  signsw0g  31726  signswmnd  31727  prodfzo03  31774  tgoldbachgt  31834  loop1cycl  32282  umgr2cycllem  32285  umgr2cycl  32286  subfacp1lem3  32327  erdsze2lem2  32349  cnpconn  32375  txpconn  32377  ptpconn  32378  indispconn  32379  connpconn  32380  cvxpconn  32387  cnllysconn  32390  cvmsss2  32419  cvmcov2  32420  cvmopnlem  32423  cvmliftlem14  32442  cvmliftlem15  32443  cvmlift2lem11  32458  cvmlift2lem12  32459  cvmlift2lem13  32460  cvmlift3lem2  32465  cvmlift3lem6  32469  cvmlift3lem9  32472  mthmi  32722  br8  32890  br6  32891  br4  32892  dfon2lem9  32934  trpredtr  32967  dftrpred3g  32970  frpomin  32976  frmin  32982  poseq  32993  wzel  33009  wsuclem  33010  wsuclb  33013  elno2  33059  sltval2  33061  noreson  33065  sltres  33067  noseponlem  33069  nolesgn2o  33076  nodense  33094  nosupfv  33104  nosupres  33105  nosupbnd1lem3  33108  nosupbnd1lem5  33110  nosupbnd2lem1  33113  noetalem3  33117  noetalem5  33119  imagesset  33312  fvtransport  33391  brcolinear  33418  brsegle  33467  seglerflx  33471  seglemin  33472  btwnsegle  33476  fvray  33500  fvline  33503  hilbert1.1  33513  elhf2  33534  0hf  33536  nn0prpwlem  33568  nn0prpw  33569  fness  33595  fneref  33596  fnessref  33603  refssfne  33604  neibastop2lem  33606  fnemeet1  33612  tailfb  33623  filnetlem4  33627  limsucncmpi  33691  taupilemrplb  34484  relowlssretop  34527  rdgellim  34540  matunitlindflem2  34771  ptrecube  34774  poimirlem4  34778  poimirlem17  34791  poimirlem20  34794  poimirlem23  34797  poimirlem24  34798  poimirlem26  34800  poimirlem27  34801  poimirlem29  34803  poimirlem32  34806  heicant  34809  mblfinlem1  34811  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  volsupnfl  34819  itg2addnclem  34825  itg2addnclem3  34827  itg2addnc  34828  ftc1anclem5  34853  unirep  34871  cover2  34872  indexa  34891  frinfm  34893  sdclem1  34901  fdc  34903  incsequz  34906  caushft  34919  istotbnd3  34932  0totbnd  34934  sstotbnd2  34935  sstotbnd  34936  sstotbnd3  34937  isbnd3  34945  ssbnd  34949  equivbnd  34951  prdsbnd  34954  prdstotbnd  34955  cntotbnd  34957  heibor1lem  34970  heiborlem1  34972  heiborlem3  34974  heiborlem6  34977  heiborlem8  34979  bfplem2  34984  rrncmslem  34993  iccbnd  35001  opidonOLD  35013  exidres  35039  isrngod  35059  isgrpda  35116  isdrngo2  35119  igenval  35222  igenidl  35224  prtlem10  35883  lshpnel2N  36003  lsmsat  36026  lssatomic  36029  lcvnbtwn  36043  lfl1  36088  eqlkr  36117  lshpkrlem1  36128  lshpkrex  36136  cvrcon3b  36295  cvrat4  36461  3dim3  36487  ps-2  36496  llni  36526  llnle  36536  lplni  36550  lplnle  36558  lplnexllnN  36582  lvoli  36593  lnatexN  36797  elpaddn0  36818  pclfinN  36918  lhprelat3N  37058  4atexlemex2  37089  4atex  37094  4atex2-0aOLDN  37096  4atex2-0cOLDN  37098  lautcvr  37110  cdleme0ex1N  37241  cdleme50rnlem  37562  cdleme50ex  37577  cdlemg1cex  37606  cdlemkid5  37953  cdlemk  37992  tendoex  37993  cdleml5N  37998  cdlemm10N  38136  dih1dimatlem0  38346  dihjat1lem  38446  dvh3dim2  38466  dvh3dim3N  38467  dochkr1  38496  dochkr1OLDN  38497  lcfrvalsnN  38559  lcfrlem27  38587  lcfrlem37  38597  lcfr  38603  mapd1o  38666  mapdpglem23  38712  hdmap11lem2  38860  resubeu  39087  nacsfix  39189  mzpcompact2lem  39228  eldioph  39235  diophrw  39236  diophin  39249  rexrabdioph  39271  rexzrexnn0  39281  eldioph4b  39288  rencldnfilem  39297  irrapxlem5  39303  irrapxlem6  39304  pell1234qrdich  39338  pell14qrdich  39346  infmrgelbi  39355  pellqrex  39356  pellfundre  39358  pellfundlb  39361  rmxynorm  39395  congrep  39450  acongrep  39457  jm2.27  39485  fnwe2lem2  39531  islssfgi  39552  hbtlem2  39604  hbtlem4  39606  hbtlem5  39608  dgraaub  39628  mpaaeu  39630  aaitgo  39642  rgspnval  39648  rgspncl  39649  clsk1independent  40276  elabrexg  41183  restuni3  41265  iinssd  41277  founiiun  41315  wessf1ornlem  41325  founiiun0  41331  unirnmap  41351  dstregt0  41427  uzfissfz  41474  fiminre2  41526  rpgtrecnn  41529  rexabslelem  41572  infrnmptle  41577  infxrunb3rnmpt  41582  infxrpnf  41601  supminfxr  41620  iooiinicc  41698  iooiinioc  41712  uzubioo  41723  climsuse  41769  islptre  41780  climinf3  41877  limsupmnfuzlem  41887  limsupre3lem  41893  limsupre3uzlem  41896  0cnv  41903  liminfreuzlem  41963  cnrefiisplem  41990  icccncfext  42050  cncficcgt0  42051  dvbdfbdioo  42095  ioodvbdlimc1lem1  42096  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  stoweidlem9  42175  stoweidlem14  42180  stoweidlem18  42184  stoweidlem21  42187  stoweidlem29  42195  stoweidlem34  42200  stoweidlem35  42201  stoweidlem39  42205  stoweidlem41  42207  stoweidlem45  42211  stoweidlem52  42218  stoweidlem55  42221  stoweidlem57  42223  stoweidlem60  42226  stirlinglem5  42244  stirlinglem13  42252  stirlinglem14  42253  fourierdlem16  42289  fourierdlem20  42293  fourierdlem21  42294  fourierdlem22  42295  fourierdlem25  42298  fourierdlem31  42304  fourierdlem39  42312  fourierdlem41  42314  fourierdlem42  42315  fourierdlem47  42319  fourierdlem48  42320  fourierdlem49  42321  fourierdlem51  42323  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem77  42349  fourierdlem81  42353  fourierdlem83  42355  fourierdlem103  42375  fourierdlem104  42376  elaa2lem  42399  etransclem47  42447  qndenserrnbl  42461  ioorrnopnlem  42470  ioorrnopnxrlem  42472  intsaluni  42493  salgencntex  42507  subsaliuncllem  42521  sge0resplit  42569  sge0seq  42609  sge0reuz  42610  nnfoctbdjlem  42618  meaiininclem  42649  hoicvrrex  42719  ovnlecvr  42721  ovnlerp  42725  hoidmv1lelem2  42755  hoidmvlelem2  42759  hoidmvlelem3  42760  ovnhoilem1  42764  ovnlecvr2  42773  hoiqssbl  42788  ovolval4lem2  42813  ovolval5lem2  42816  ovnovollem1  42819  ovnovollem2  42820  iinhoiicclem  42836  smfinflem  42972  smflimsuplem7  42981  sprsymrelfolem2  43502  perfectALTV  43735  9gbo  43786  11gbo  43787  nnsum3primes4  43800  nnsum3primesprm  43802  ssnn0ssfz  44295  lincsumcl  44384  lincscmcl  44385  zlmodzxzldep  44457  ldepsnlinc  44461  line2ylem  44636  line2xlem  44638  aacllem  44800
  Copyright terms: Public domain W3C validator