MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexbidv Unicode version

Theorem rexbidv 2968
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.)
Hypothesis
Ref Expression
rexbidv.1
Assertion
Ref Expression
rexbidv
Distinct variable group:   ,

Proof of Theorem rexbidv
StepHypRef Expression
1 rexbidv.1 . . 3
21adantr 465 . 2
32rexbidva 2965 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  rexbiiOLD  2970  2rexbidv  2975  rexralbidv  2976  rexeqbi1dv  3063  rexeqbidv  3069  cbvrex2v  3093  rspc2ev  3221  rspc3ev  3223  ceqsrex2v  3235  sbcrexgOLD  3413  uniiunlem  3587  rabasiun  4334  eliun  4335  dfiin2g  4363  dfiunv2  4366  elrnmpt  5254  elrnmptg  5257  elimag  5346  fvelrnb  5920  fvelimab  5929  foelrn  6050  foco2  6051  elabrex  6155  abrexco  6156  f1oiso  6247  f1oiso2  6248  grprinvlem  6513  orduninsuc  6678  funcnvuni  6753  fun11iun  6760  abrexex2g  6777  abrexex2  6781  f1oweALT  6784  el2xptp  6843  recseq  7062  tfrlem12  7077  seqomlem2  7135  nneob  7320  qseq2  7381  elqsg  7382  elixpsn  7528  ixpsnf1o  7529  isfi  7559  enfi  7756  pssnn  7758  frfi  7785  unblem1  7792  unblem2  7793  unbnn2  7797  fofinf1o  7821  finsschain  7847  indexfi  7848  elfi  7893  marypha1lem  7913  supeq3  7929  supmo  7932  suplub  7940  supisolem  7952  oieq1  7958  ordtypelem2  7965  ordtypelem3  7966  ordtypelem9  7972  wemaplem1  7992  brwdom2  8020  brwdom3  8029  unwdomg  8031  oemapval  8123  cantnf  8133  cantnfOLD  8155  wemapwe  8160  wemapweOLD  8161  cnfcom3clem  8170  cnfcom3clemOLD  8178  tz9.13  8230  tz9.13g  8231  cardf2  8345  isnum2  8347  ennum  8349  cardiun  8384  infxpenc2  8420  infxpenc2OLD  8424  aceq1  8519  aceq2  8521  dfac5lem3  8527  dfac5lem4  8528  dfac2a  8531  dfac2  8532  kmlem9  8559  kmlem12  8562  kmlem14  8564  ackbij1  8639  cflm  8651  cfss  8666  cofsmo  8670  cfsmolem  8671  cfcoflem  8673  coftr  8674  isfin7  8702  fin23lem26  8726  isf32lem5  8758  fin1a2lem11  8811  hsmexlem2  8828  axdc3lem3  8853  axdc3  8855  numthcor  8895  zorn2lem7  8903  brdom3  8927  brdom7disj  8930  brdom6disj  8931  iundom2g  8936  fpwwe2  9042  winainflem  9092  winalim2  9095  inar1  9174  tskuni  9182  nqereu  9328  prnmax  9394  genpv  9398  genpnmax  9406  genpass  9408  prlem936  9446  recexsrlem  9501  map2psrpr  9508  supsrlem  9509  axrrecex  9561  axpre-sup  9567  dedekind  9765  cnegex  9782  recex  10206  fimaxre3  10517  infm3  10527  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  creur  10555  creui  10556  cju  10557  nnunb  10816  arch  10817  xrsupsslem  11527  xrinfmsslem  11528  xrsupss  11529  xrinfmss  11530  xrub  11532  supxrunb1  11540  supxrunb2  11541  infmxrgelb  11555  fsequb2  12086  iswrd  12550  wrdval  12551  csbwrdg  12570  cshword  12762  0csh0  12764  2cshwcshw  12793  scshwfzeqfzo  12794  shftfval  12903  abs1m  13168  rexfiuz  13180  limsupbnd2  13306  clim  13317  rlim  13318  rlim2  13319  rlim0  13331  rlim0lt  13332  ello1mpt2  13345  o1lo1  13360  o1compt  13410  rlimdiv  13468  climsup  13492  sumeq1  13511  sumeq2w  13514  summo  13539  fsum  13542  fsumcvg3  13551  infcvgaux2i  13669  mertenslem1  13693  mertenslem2  13694  mertens  13695  prodeq1f  13715  prodeq2w  13719  prodmo  13743  fprod  13748  divides  13988  odd2np1lem  14045  divalglem4  14054  divalglem10  14060  divalg  14061  gcdcllem3  14151  bezoutlem1  14176  exprmfct  14251  nnnn0modprm0  14331  opeo  14337  omeo  14338  pythagtriplem2  14341  pythagtrip  14358  pceu  14370  pcprmpw2  14405  unbenlem  14426  4sqlem12  14474  vdwapval  14491  vdwapun  14492  vdwmc2  14497  vdwpc  14498  vdwlem2  14500  vdwlem10  14508  vdwlem13  14511  vdwnnlem1  14513  rami  14533  cshwsiun  14584  cshwrepswhash1  14587  brssc  15183  isdrs  15563  drsdir  15564  drsdirfi  15567  isdrs2  15568  ipodrsima  15795  gsumvalx  15897  gsumpropd  15899  gsumress  15903  isnsgrp  15915  sgrp2nmndlem5  16047  grpinvex  16065  grp1  16142  imasgrp2  16185  conjnmzb  16301  gaorb  16345  orbsta  16351  symgfix2  16441  symgextfo  16447  pmtrprfvalrn  16513  psgnunilem3  16521  psgneu  16531  psgnval  16532  psgnvali  16533  psgnvalii  16534  ispgp  16612  subgpgp  16617  sylow1  16623  pgpfi  16625  sylow2blem3  16642  fislw  16645  sylow3lem2  16648  lsmelvalm  16671  lsmass  16688  pj1fval  16712  pj1val  16713  pj1eu  16714  pj1id  16717  efgrelexlema  16767  efgrelexlemb  16768  efgredeu  16770  cyggeninv  16886  cygabl  16893  pgpfac1lem2  17126  pgpfac1lem3  17128  pgpfac1lem4  17129  pgpfac1  17131  pgpfaclem2  17133  pgpfac  17135  dvdsrval  17294  dvdsr  17295  subrgdvds  17443  lss1d  17609  lspsn  17648  lspsnel  17649  lspsolvlem  17788  rspsn  17902  opsrval  18139  znf1o  18590  cygznlem3  18608  psgndiflemA  18637  ellspd  18836  ellspdOLD  18837  mat1dimelbas  18973  mat1dimbas  18974  scmatval  19006  scmatel  19007  scmateALT  19014  mat0scmat  19040  decpmataa0  19269  decpmatmulsumfsupp  19274  pmatcollpw2lem  19278  pm2mpmhmlem1  19319  chpscmat  19343  basis2  19452  eltg2  19459  tg2  19466  isclo  19588  neival  19603  isnei  19604  isneip  19606  restbas  19659  neitr  19681  cnpval  19737  iscnp  19738  cnpimaex  19757  lmbr  19759  lmbr2  19760  cnprest2  19791  lmff  19802  regsep  19835  pnrmopn  19844  nrmsep3  19856  isnrm2  19859  iscmp  19888  cmpsublem  19899  cmpsub  19900  tgcmp  19901  sscmp  19905  hauscmplem  19906  1stcclb  19945  1stcfb  19946  is2ndc  19947  2ndc1stc  19952  1stcrest  19954  2ndcctbss  19956  1stcelcls  19962  llyeq  19971  nllyeq  19972  hausllycmp  19995  lly1stc  19997  refssex  20012  refun0  20016  islocfin  20018  locfinnei  20024  comppfsc  20033  txbas  20068  ptval  20071  ptpjopn  20113  ptclsg  20116  txcnp  20121  ptcnp  20123  txrest  20132  ptrescn  20140  txcmp  20144  tx1stc  20151  xkococn  20161  kqreglem1  20242  fbasssin  20337  fbssfi  20338  fbssint  20339  fbun  20341  fgss2  20375  fgcl  20379  ufli  20415  fmfnfmlem3  20457  fbflim2  20478  hauspwpwf1  20488  flfneii  20493  flftg  20497  txflf  20507  fclscf  20526  alexsubb  20546  alexsubALT  20551  tsmssubm  20644  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ust0  20722  trust  20732  elutop  20736  ucnval  20780  ucncn  20788  cfiluexsm  20793  cfiluweak  20798  blssps  20927  blss  20928  imasf1oxms  20992  mopni  20995  metss  21011  metrest  21027  metcnp3  21043  cfilucfilOLD  21072  cfilucfil  21073  metuel2  21082  nlmvscn  21196  nrginvrcn  21200  icccmplem1  21327  icccmplem2  21328  icccmp  21330  divcn  21372  cncfval  21392  elcncf2  21394  cncfmet  21412  cnheibor  21455  evth  21459  lebnumlem3  21463  lebnum  21464  xlebnum  21465  lebnumii  21466  ipcn  21686  lmmbr  21697  lmmbr2  21698  cfilfval  21703  cfili  21707  iscfil3  21712  caufval  21714  iscau  21715  iscau2  21716  equivcfil  21738  equivcau  21739  lmcau  21751  ovolval  21885  elovolm  21886  ovolgelb  21891  ovoliunlem1  21913  ovoliun2  21917  ovolshftlem1  21920  ovolscalem1  21924  ovolicc  21934  ioombl1lem4  21971  uniioombllem2  21992  mbfaddlem  22067  mbfsup  22071  mbfinf  22072  mbflimsup  22073  i1fmulc  22110  itg1climres  22121  itg2val  22135  itg2l  22136  itg2leub  22141  itg2seq  22149  itg2monolem1  22157  itg2mono  22160  itg2i1fseq2  22163  cniccibl  22247  ellimc3  22283  limciun  22298  dvferm1  22386  dvferm2  22388  lhop1lem  22414  ply1divex  22537  ig1peu  22572  plyval  22590  elply2  22593  coeval  22620  coeeu  22622  coelem  22623  coeeq  22624  plydivlem4  22692  plydivex  22693  aannenlem2  22725  aalioulem2  22729  aaliou2  22736  ulmval  22775  ulm2  22780  ulmcau  22790  ulmdvlem3  22797  abelthlem9  22835  abelth  22836  efif1olem4  22932  eflogeq  22986  efopn  23039  cxpcn3  23122  cxpeq  23131  rlimcnp  23295  muval  23406  dchrptlem1  23539  dchrptlem2  23540  lgsdchrval  23622  pntpbnd  23773  pntibndlem3  23777  pntibnd  23778  pntlemi  23789  pntleme  23793  pntlemp  23795  pnt3  23797  istrkgld  23857  axtgsegcon  23861  axtgpasch  23864  axtgcont1  23865  legov  23972  islnopp  24113  ishpg  24128  hpgbr  24129  hpgcom  24136  ttgval  24178  ttgitvval  24185  ttgelitv  24186  brbtwn  24202  brcgr  24203  axpasch  24244  axlowdim2  24263  axlowdim  24264  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  nbgraf1olem1  24441  cusgrafilem2  24480  cusgrafi  24482  wwlkn0  24689  clwwlknscsh  24819  erclwwlkneq  24823  eclclwwlkn0  24831  eleclclwwlkn  24833  hashecclwwlkn1  24834  usghashecclwwlk  24835  el2wlksot  24880  el2pthsot  24881  2spot2iun2spont  24891  iseupa  24965  3cyclfrgrarn1  25012  usgn0fidegnn0  25029  frgrancvvdeqlem4  25033  friendshipgt3  25121  isgrpo  25198  isgrpoi  25200  grpoidinvlem3  25208  grpoideu  25211  grpoidinv2  25220  isgrp2d  25237  isgrpda  25299  ghgrpOLD  25370  rngoid  25385  nmoofval  25677  nmooval  25678  nmosetn0  25680  nmoolb  25686  nmoubi  25687  nmlno0lem  25708  chcompl  26160  pjhthmo  26220  pjhval  26315  pjpreeq  26316  h1de2ci  26474  elspansn  26484  nmopval  26775  nmopsetn0  26784  nmfnval  26795  nmfnsetn0  26797  eigvecval  26815  hhcno  26823  hhcnf  26824  nmoplb  26826  nmopub  26827  nmfnlb  26843  nmfnleub  26844  eleigvec  26876  nmlnop0iALT  26914  nmopun  26933  nmcexi  26945  branmfn  27024  pjnmopi  27067  cvbr  27201  hatomic  27279  chrelat2  27289  cdjreui  27351  cdj3lem2  27354  reuxfr4d  27389  elabreximd  27408  br8d  27463  unipreima  27484  abfmpunirn  27490  curry2ima  27526  toslublem  27655  tosglblem  27657  archirng  27732  archiexdiv  27734  archiabllem2a  27738  archiabl  27742  isarchiofld  27807  crefi  27850  pcmplfin  27863  pstmfval  27875  tpr2rico  27894  rge0scvg  27931  ismntop  28004  esumc  28062  esumpcvgval  28084  dya2icoseg2  28249  dya2iocuni  28254  eulerpartlemgvv  28315  eulerpartlemgh  28317  lgamgulmlem6  28576  subfacp1lem3  28626  pconcn  28669  cnpcon  28675  txpcon  28677  conpcon  28680  iscvm  28704  cvmcov  28708  cvmopnlem  28723  cvmliftlem15  28743  cvmlift3lem2  28765  cvmlift3lem4  28767  cvmlift3  28773  br8  29185  br6  29186  br4  29187  dfrdg2  29228  dfrdg3  29229  orderseqlem  29332  poseq  29333  soseq  29334  elno  29406  sltval  29407  nobndlem6  29457  nofulllem1  29462  nofulllem2  29463  nofulllem5  29466  altxpeq2  29624  funtransport  29681  fvtransport  29682  brcolinear2  29708  colineardim1  29711  segcon2  29755  brsegle  29758  funray  29790  fvray  29791  funline  29792  linedegen  29793  fvline  29794  ellines  29802  supaddc  30041  supadd  30042  ptrest  30048  heicant  30049  mblfinlem1  30051  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  cnicciblnc  30086  ftc1anclem6  30095  gtinf  30137  nn0prpwlem  30140  fnessref  30175  neibastop2lem  30178  neibastop2  30179  tailfb  30195  unirep  30203  indexa  30224  sdclem2  30235  sdclem1  30236  sdc  30237  fdc  30238  fdc1  30239  incsequz  30241  istotbnd  30265  sstotbnd2  30270  equivtotbnd  30274  isbnd  30276  bndss  30282  ssbnd  30284  totbndbnd  30285  ismtybndlem  30302  heibor1lem  30305  heiborlem1  30307  heiborlem6  30312  heiborlem8  30314  heiborlem10  30316  heibor  30317  isdrngo2  30361  divrngidl  30425  prnc  30464  isfldidl  30465  prtlem5  30597  prtlem13  30609  prtlem16  30610  elrfi  30626  isnacs  30636  nacsfg  30637  nacsfix  30644  mzpcompact2lem  30684  eldiophb  30690  eldioph  30691  eldioph2  30695  eldioph2b  30696  eldioph3  30699  eldiophss  30708  diophrex  30709  sbc2rexgOLD  30721  rexrabdioph  30727  rexfrabdioph  30728  elnn0rabdioph  30736  dvdsrabdioph  30743  eldioph4b  30745  eldioph4i  30746  diophren  30747  rencldnfilem  30754  pell1234qrdich  30797  jm2.27  30950  expdiophlem1  30963  wepwsolem  30987  aomclem8  31007  islnr3  31064  lnr2i  31065  lpirlnr  31066  hbtlem1  31072  hbtlem2  31073  hbtlem7  31074  hbtlem4  31075  hbtlem5  31077  hbtlem6  31078  dgraaval  31093  dgraalem  31094  dgraaub  31097  rngunsnply  31122  elabrexg  31430  upbdrech  31505  ssfiunibd  31509  iccshift  31558  iooshift  31562  infrglb  31584  climinf  31612  climinff  31617  ellimcabssub0  31623  climf  31628  limcperiod  31634  limclner  31657  cncfshiftioo  31695  fperdvper  31715  itgiccshift  31779  itgperiod  31780  stoweidlem27  31809  stoweidlem31  31813  stoweidlem43  31825  stoweidlem46  31828  stoweidlem52  31834  stoweidlem60  31842  fourierdlem42  31931  fourierdlem48  31937  fourierdlem51  31940  fourierdlem54  31943  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem68  31957  fourierdlem70  31959  fourierdlem71  31960  fourierdlem73  31962  fourierdlem80  31969  fourierdlem81  31970  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem100  31989  fourierdlem103  31992  fourierdlem104  31993  fourierdlem105  31994  fourierdlem108  31997  fourierdlem109  31998  fourierdlem110  31999  fourierdlem112  32001  fourierdlem113  32002  cbvrex2  32178  afvelrnb  32248  afvelrnb0  32249  0nodd  32498  1odd  32499  2nodd  32500  0even  32737  1neven  32738  2even  32739  2zlidl  32740  2zrngamgm  32745  2zrngagrp  32749  2zrngmmgm  32752  2zrngnmrid  32756  lcoval  33013  el0ldep  33067  ldepspr  33074  zlmodzxzldep  33105  bnj66  33918  bnj873  33982  bnj18eq1  33985  bnj1234  34069  bnj1318  34081  bj-finsumval0  34663  islshp  34704  lsmsat  34733  lcvbr  34746  lsatcv0  34756  lshpsmreu  34834  lshpkrlem1  34835  lshpkrlem2  34836  lshpkrlem3  34837  lshpkrcl  34841  lshpset2N  34844  islshpkrN  34845  cvrval  34994  atlex  35041  glbconxN  35102  hlsuprexch  35105  islln  35230  islpln  35254  islpln5  35259  lvolex3N  35262  islvol  35297  islvol5  35303  ispointN  35466  pmapglbx  35493  paddval  35522  elpaddn0  35524  elpaddat  35528  elpadd0  35533  4atex  35800  4atex2  35801  cdlemefrs29bpre1  36123  cdlemefrs32fva  36126  cdlemg33b  36433  dvhb1dimN  36712  dvhopellsm  36844  dib1dim  36892  diclspsn  36921  dihglblem2aN  37020  dihglblem2N  37021  dih1dimatlem  37056  dvh3dimatN  37166  dvh2dim  37172  dvh3dim  37173  dvh4dimN  37174  dvh3dim3N  37176  dochfl1  37203  lcfl7N  37228  lcf1o  37278  lcfrlem39  37308  mapdpglem3  37402  hvmapvalvalN  37488  hdmap14lem2a  37597  hdmapglem7a  37657  extoimad  37981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-rex 2813
  Copyright terms: Public domain W3C validator