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

Theorem rexbidv 3081
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:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidv
StepHypRef Expression
1 rexbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 480 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexbidva 3078 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-rex 2947
This theorem is referenced by:  2rexbidv  3086  rexralbidv  3087  rexeqbi1dv  3177  rexeqbidv  3183  cbvrex2v  3210  rspc2ev  3355  rspc3ev  3357  ceqsrex2v  3369  uniiunlem  3724  n0snor2el  4396  eliun  4556  dfiin2g  4585  dfiunv2  4588  elrnmpt  5404  elrnmptg  5407  elimag  5505  fvelrnb  6282  fvelimab  6292  foelrn  6418  foco2  6419  foco2OLD  6420  elabrex  6541  abrexco  6542  f1oiso  6641  f1oiso2  6642  grprinvlem  6914  orduninsuc  7085  funcnvuni  7161  fun11iun  7168  abrexex2g  7186  abrexex2OLD  7192  f1oweALT  7194  el2xptp  7255  tfrlem12  7530  seqomlem2  7591  nneob  7777  qseq2  7840  elqsg  7841  elqsecl  7844  elixpsn  7989  ixpsnf1o  7990  isfi  8021  enfi  8217  pssnn  8219  frfi  8246  unblem1  8253  unblem2  8254  unbnn2  8258  fofinf1o  8282  finsschain  8314  indexfi  8315  elfi  8360  marypha1lem  8380  supeq3  8396  supmo  8399  suplub  8407  supisolem  8420  eqinf  8431  infval  8433  infglb  8437  infglbb  8438  infmo  8442  oieq1  8458  ordtypelem2  8465  ordtypelem3  8466  ordtypelem9  8472  wemaplem1  8492  brwdom2  8519  brwdom3  8528  unwdomg  8530  oemapval  8618  cantnf  8628  wemapwe  8632  cnfcom3clem  8640  tz9.13  8692  tz9.13g  8693  cardf2  8807  isnum2  8809  ennum  8811  cardiun  8846  infxpenc2  8883  aceq1  8978  aceq2  8980  dfac5lem3  8986  dfac5lem4  8987  dfac2a  8990  dfac2  8991  kmlem9  9018  kmlem12  9021  kmlem14  9023  ackbij1  9098  cflm  9110  cfss  9125  cofsmo  9129  cfsmolem  9130  cfcoflem  9132  coftr  9133  isfin7  9161  fin23lem26  9185  isf32lem5  9217  fin1a2lem11  9270  hsmexlem2  9287  axdc3lem3  9312  axdc3  9314  numthcor  9354  zorn2lem7  9362  brdom3  9388  brdom7disj  9391  brdom6disj  9392  iundom2g  9400  fpwwe2  9503  winainflem  9553  winalim2  9556  inar1  9635  tskuni  9643  nqereu  9789  prnmax  9855  genpv  9859  genpnmax  9867  genpass  9869  prlem936  9907  recexsrlem  9962  map2psrpr  9969  supsrlem  9970  axrrecex  10022  axpre-sup  10028  dedekind  10238  cnegex  10255  recex  10697  fimaxre3  11008  infm3  11020  supaddc  11028  supadd  11029  supmul1  11030  supmullem1  11031  supmullem2  11032  supmul  11033  creur  11052  creui  11053  cju  11054  nnunb  11326  arch  11327  xrsupsslem  12175  xrinfmsslem  12176  xrsupss  12177  xrinfmss  12178  xrub  12180  supxrunb1  12187  supxrunb2  12188  infmremnf  12211  infmrp1  12212  modmuladd  12752  fsequb2  12815  hashge2el2difr  13301  iswrd  13339  wrdval  13340  csbwrdg  13366  cshword  13583  0csh0  13585  2cshwcshw  13617  scshwfzeqfzo  13618  cshimadifsn  13621  shftfval  13854  abs1m  14119  rexfiuz  14131  limsupbnd2  14258  clim  14269  rlim  14270  rlim2  14271  rlim0  14283  rlim0lt  14284  ello1mpt2  14297  o1lo1  14312  o1compt  14362  rlimdiv  14420  climsup  14444  sumeq1  14463  sumeq2w  14466  summo  14492  fsum  14495  fsumcvg3  14504  infcvgaux2i  14634  mertenslem1  14660  mertenslem2  14661  mertens  14662  prodeq1f  14682  prodeq2w  14686  prodmo  14710  fprod  14715  divides  15029  odd2np1lem  15111  opeo  15136  omeo  15137  divalglem4  15166  divalglem10  15172  divalg  15173  gcdcllem3  15270  zeqzmulgcd  15279  bezoutlem1  15303  exprmfct  15463  nnnn0modprm0  15558  pythagtriplem2  15569  pythagtrip  15586  pceu  15598  pcprmpw2  15633  unbenlem  15659  4sqlem12  15707  vdwapval  15724  vdwapun  15725  vdwmc2  15730  vdwpc  15731  vdwlem2  15733  vdwlem10  15741  vdwlem13  15744  vdwnnlem1  15746  rami  15766  cshwsiun  15853  cshwrepswhash1  15856  brssc  16521  isdrs  16981  drsdir  16982  drsdirfi  16985  isdrs2  16986  ipodrsima  17212  gsumvalx  17317  gsumpropd  17319  gsumress  17323  isnsgrp  17335  sgrp2nmndlem5  17463  grpinvex  17479  dfgrp2  17494  grpidinv2  17521  grpidinv  17522  dfgrp3lem  17560  grp1  17569  imasgrp2  17577  conjnmzb  17742  gaorb  17786  orbsta  17792  symgfix2  17882  symgextfo  17888  pmtrprfvalrn  17954  psgnunilem3  17962  psgneu  17972  psgnval  17973  psgnvali  17974  psgnvalii  17975  ispgp  18053  subgpgp  18058  sylow1  18064  pgpfi  18066  sylow2blem3  18083  fislw  18086  sylow3lem2  18089  lsmelvalm  18112  lsmass  18129  pj1fval  18153  pj1val  18154  pj1eu  18155  pj1id  18158  efgrelexlema  18208  efgrelexlemb  18209  efgredeu  18211  cyggeninv  18331  cygabl  18338  pgpfac1lem2  18520  pgpfac1lem3  18522  pgpfac1lem4  18523  pgpfac1  18525  pgpfaclem2  18527  pgpfac  18529  dvdsrval  18691  dvdsr  18692  subrgdvds  18842  lss1d  19011  lspsn  19050  lspsnel  19051  lspsolvlem  19190  rspsn  19302  opsrval  19522  znf1o  19948  cygznlem3  19966  psgndiflemA  19995  ellspd  20189  mat1dimelbas  20325  mat1dimbas  20326  scmatval  20358  scmatel  20359  scmateALT  20366  mat0scmat  20392  decpmataa0  20621  decpmatmulsumfsupp  20626  pmatcollpw2lem  20630  pm2mpmhmlem1  20671  chpscmat  20695  basis2  20803  eltg2  20810  tg2  20817  isclo  20939  neival  20954  isnei  20955  isneip  20957  restbas  21010  neitr  21032  cnpval  21088  iscnp  21089  cnpimaex  21108  lmbr  21110  lmbr2  21111  cnprest2  21142  lmff  21153  regsep  21186  pnrmopn  21195  nrmsep3  21207  isnrm2  21210  iscmp  21239  cmpsublem  21250  cmpsub  21251  tgcmp  21252  sscmp  21256  hauscmplem  21257  1stcclb  21295  1stcfb  21296  is2ndc  21297  2ndc1stc  21302  1stcrest  21304  2ndcctbss  21306  1stcelcls  21312  llyeq  21321  nllyeq  21322  hausllycmp  21345  lly1stc  21347  refssex  21362  refun0  21366  islocfin  21368  locfinnei  21374  comppfsc  21383  txbas  21418  ptval  21421  ptpjopn  21463  ptclsg  21466  txcnp  21471  ptcnp  21473  txrest  21482  ptrescn  21490  txcmp  21494  tx1stc  21501  xkococn  21511  kqreglem1  21592  fbasssin  21687  fbssfi  21688  fbssint  21689  fbun  21691  fgss2  21725  fgcl  21729  ufli  21765  fmfnfmlem3  21807  fbflim2  21828  hauspwpwf1  21838  flfneii  21843  flftg  21847  txflf  21857  fclscf  21876  alexsubb  21897  alexsubALT  21902  tsmssubm  21993  ustincl  22058  ustdiag  22059  ustinvel  22060  ustexhalf  22061  ust0  22070  trust  22080  elutop  22084  ucnval  22128  ucncn  22136  cfiluexsm  22141  cfiluweak  22146  blssps  22276  blss  22277  imasf1oxms  22341  mopni  22344  metss  22360  metrest  22376  metcnp3  22392  cfilucfil  22411  metuel2  22417  nlmvscn  22538  nrginvrcn  22543  icccmplem1  22672  icccmplem2  22673  icccmp  22675  divcn  22718  cncfval  22738  elcncf2  22740  cncfmet  22758  cnheibor  22801  evth  22805  lebnumlem3  22809  lebnum  22810  xlebnum  22811  lebnumii  22812  ipcn  23091  lmmbr  23102  lmmbr2  23103  cfilfval  23108  cfili  23112  iscfil3  23117  caufval  23119  iscau  23120  iscau2  23121  equivcfil  23143  equivcau  23144  lmcau  23157  ovolval  23288  elovolm  23289  ovolgelb  23294  ovoliunlem1  23316  ovoliun2  23320  ovolshftlem1  23323  ovolscalem1  23327  ovolicc  23337  ioombl1lem4  23375  uniioombllem2  23397  mbfaddlem  23472  mbfsup  23476  mbfinf  23477  mbflimsup  23478  i1fmulc  23515  itg1climres  23526  itg2val  23540  itg2l  23541  itg2leub  23546  itg2seq  23554  itg2monolem1  23562  itg2mono  23565  itg2i1fseq2  23568  cniccibl  23652  ellimc3  23688  limciun  23703  dvferm1  23793  dvferm2  23795  lhop1lem  23821  ply1divex  23941  ig1peu  23976  plyval  23994  elply2  23997  coeval  24024  coeeu  24026  coelem  24027  coeeq  24028  plydivlem4  24096  plydivex  24097  aannenlem2  24129  aalioulem2  24133  aaliou2  24140  ulmval  24179  ulm2  24184  ulmcau  24194  ulmdvlem3  24201  abelthlem9  24239  abelth  24240  efif1olem4  24336  eflogeq  24393  efopn  24449  cxpcn3  24534  cxpeq  24543  rlimcnp  24737  lgamgulmlem6  24805  muval  24903  dchrptlem1  25034  dchrptlem2  25035  lgsdchrval  25124  2lgslem1b  25162  pntpbnd  25322  pntibndlem3  25326  pntibnd  25327  pntlemi  25338  pntleme  25342  pntlemp  25344  pnt3  25346  istrkgld  25403  istrkg3ld  25405  axtgsegcon  25408  axtgpasch  25411  axtgcont1  25412  axtgupdim2  25415  legov  25525  islnopp  25676  ishpg  25696  hpgbr  25697  hpgcom  25704  iscgra  25746  iscgra1  25747  isinag  25774  isleag  25778  ttgval  25800  ttgitvval  25807  ttgelitv  25808  brbtwn  25824  brcgr  25825  axpasch  25866  axlowdim2  25885  axlowdim  25886  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  upgredg2vtx  26081  edglnl  26083  usgredg4  26154  ushgredgedg  26166  ushgredgedgloop  26168  dfnbgr2  26275  nbgrel  26278  nbgrelOLD  26279  nbumgrvtx  26287  nbgrnself  26300  uvtxel1  26345  uvtxael1OLD  26347  uvtxa01vtx0OLD  26348  cusgrfilem2  26408  cusgrfi  26410  vtxd0nedgb  26440  fusgrn0degnn0  26451  wlkonl1iedg  26617  wspniunwspnon  26888  elwwlks2on  26925  clwwlknscsh  27027  erclwwlkneq  27031  eleclclwwlkn  27040  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  3cyclfrgrrn1  27265  friendshipgt3  27385  isgrpo  27479  isgrpoi  27480  grpoidinvlem3  27488  grpoideu  27491  grpoidinv2  27497  nmoofval  27745  nmooval  27746  nmosetn0  27748  nmoolb  27754  nmoubi  27755  nmlno0lem  27776  chcompl  28227  pjhthmo  28289  pjhval  28384  pjpreeq  28385  h1de2ci  28543  elspansn  28553  nmopval  28843  nmopsetn0  28852  nmfnval  28863  nmfnsetn0  28865  eigvecval  28883  hhcno  28891  hhcnf  28892  nmoplb  28894  nmopub  28895  nmfnlb  28911  nmfnleub  28912  eleigvec  28944  nmlnop0iALT  28982  nmopun  29001  nmcexi  29013  branmfn  29092  pjnmopi  29135  cvbr  29269  hatomic  29347  chrelat2  29357  cdjreui  29419  cdj3lem2  29422  reuxfr4d  29457  elabreximd  29474  br8d  29548  unipreima  29574  abfmpunirn  29580  curry2ima  29614  toslublem  29795  tosglblem  29797  archirng  29870  archiexdiv  29872  archiabllem2a  29876  archiabl  29880  isarchiofld  29945  crefi  30042  pcmplfin  30055  pstmfval  30067  tpr2rico  30086  rge0scvg  30123  ismntop  30198  esumc  30241  esumpcvgval  30268  esum2dlem  30282  inelsros  30369  diffiunisros  30370  dya2icoseg2  30468  dya2iocuni  30473  eulerpartlemgvv  30566  eulerpartlemgh  30568  hgt749d  30855  tgoldbachgt  30869  bnj66  31056  bnj873  31120  bnj18eq1  31123  bnj1234  31207  bnj1318  31219  subfacp1lem3  31290  pconncn  31332  cnpconn  31338  txpconn  31340  connpconn  31343  iscvm  31367  cvmcov  31371  cvmopnlem  31386  cvmliftlem15  31406  cvmlift3lem2  31428  cvmlift3lem4  31430  cvmlift3  31436  br8  31772  br6  31773  br4  31774  dfrdg2  31825  dfrdg3  31826  orderseqlem  31877  poseq  31878  soseq  31879  elno  31924  sltval  31925  noprefixmo  31973  nosupno  31974  nosupdm  31975  nosupfv  31977  nosupres  31978  nosupbnd1lem1  31979  nosupbnd1lem3  31981  nosupbnd1lem4  31982  nosupbnd1lem5  31983  noeta  31993  altxpeq2  32206  funtransport  32263  fvtransport  32264  brcolinear2  32290  colineardim1  32293  segcon2  32337  brsegle  32340  funray  32372  fvray  32373  funline  32374  linedegen  32375  fvline  32376  ellines  32384  gtinfOLD  32439  nn0prpwlem  32442  fnessref  32477  neibastop2lem  32480  neibastop2  32481  tailfb  32497  unblimceq0lem  32622  unblimceq0  32623  unbdqndv2  32627  bj-finsumval0  33277  relowlssretop  33341  phpreu  33523  matunitlindflem2  33536  ptrest  33538  poimirlem4  33543  poimirlem17  33556  poimirlem20  33559  poimirlem24  33563  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem31  33570  poimirlem32  33571  poimir  33572  heicant  33574  mblfinlem1  33576  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  cnicciblnc  33611  ftc1anclem6  33620  unirep  33637  indexa  33658  sdclem2  33668  sdclem1  33669  sdc  33670  fdc  33671  fdc1  33672  incsequz  33674  istotbnd  33698  sstotbnd2  33703  equivtotbnd  33707  isbnd  33709  bndss  33715  ssbnd  33717  totbndbnd  33718  ismtybndlem  33735  heibor1lem  33738  heiborlem1  33740  heiborlem6  33745  heiborlem8  33747  heiborlem10  33749  heibor  33750  rngoid  33831  isgrpda  33884  isdrngo2  33887  divrngidl  33957  prnc  33996  isfldidl  33997  exanres3  34205  brcoels  34330  br1cossxrnres  34338  eldm1cossres2  34351  prtlem5  34464  prtlem13  34472  prtlem16  34473  islshp  34584  lsmsat  34613  lcvbr  34626  lsatcv0  34636  lshpsmreu  34714  lshpkrlem1  34715  lshpkrlem2  34716  lshpkrlem3  34717  lshpkrcl  34721  lshpset2N  34724  islshpkrN  34725  cvrval  34874  atlex  34921  glbconxN  34982  hlsuprexch  34985  islln  35110  islpln  35134  islpln5  35139  lvolex3N  35142  islvol  35177  islvol5  35183  ispointN  35346  pmapglbx  35373  paddval  35402  elpaddn0  35404  elpaddat  35408  elpadd0  35413  4atex  35680  4atex2  35681  cdlemefrs29bpre1  36002  cdlemefrs32fva  36005  cdlemg33b  36312  dvhb1dimN  36591  dvhopellsm  36723  dib1dim  36771  diclspsn  36800  dihglblem2aN  36899  dihglblem2N  36900  dih1dimatlem  36935  dvh3dimatN  37045  dvh2dim  37051  dvh3dim  37052  dvh4dimN  37053  dvh3dim3N  37055  dochfl1  37082  lcfl7N  37107  lcf1o  37157  lcfrlem39  37187  mapdpglem3  37281  hvmapvalvalN  37367  hdmap14lem2a  37476  hdmapglem7a  37536  elrfi  37574  isnacs  37584  nacsfg  37585  nacsfix  37592  mzpcompact2lem  37631  eldiophb  37637  eldioph  37638  eldioph2  37642  eldioph2b  37643  eldioph3  37646  eldiophss  37655  diophrex  37656  sbcrexgOLD  37666  sbc2rexgOLD  37669  rexrabdioph  37675  rexfrabdioph  37676  elnn0rabdioph  37684  dvdsrabdioph  37691  eldioph4b  37692  eldioph4i  37693  diophren  37694  rencldnfilem  37701  pell1234qrdich  37742  jm2.27  37892  expdiophlem1  37905  wepwsolem  37929  aomclem8  37948  islnr3  38002  lnr2i  38003  lpirlnr  38004  hbtlem1  38010  hbtlem2  38011  hbtlem7  38012  hbtlem4  38013  hbtlem5  38015  hbtlem6  38016  dgraaval  38031  dgraalem  38032  dgraaub  38035  rngunsnply  38060  brtrclfv2  38336  clsk1indlem1  38660  extoimad  38781  elabrexg  39520  foelrnf  39687  disjrnmpt2  39689  upbdrech  39833  ssfiunibd  39837  supxrgere  39862  supxrgelem  39866  supxrge  39867  suplesup  39868  infxr  39896  infleinf  39901  supxrunb3  39936  unb2ltle  39955  uzub  39971  supminfxr  40007  iccshift  40062  iooshift  40066  climinf  40156  climinff  40161  ellimcabssub0  40167  climf  40172  limcperiod  40178  limclner  40201  climf2  40216  clim2d  40223  limsupref  40235  limsuppnfd  40252  limsuppnf  40261  climinfmpt  40265  limsupubuzmpt  40269  limsupmnf  40271  limsupre2lem  40274  limsupre2  40275  limsupmnfuz  40277  limsupre2mpt  40280  limsupre3lem  40282  limsupre3  40283  limsupre3mpt  40284  limsupre3uzlem  40285  limsupre3uz  40286  limsupreuz  40287  limsupreuzmpt  40289  climuz  40294  liminfreuzlem  40352  liminfreuz  40353  xlimmnfvlem1  40376  xlimmnfv  40378  xlimpnfvlem1  40380  xlimpnfv  40382  cncfshiftioo  40423  fperdvper  40451  itgiccshift  40514  itgperiod  40515  stoweidlem27  40562  stoweidlem31  40566  stoweidlem43  40578  stoweidlem46  40581  stoweidlem52  40587  stoweidlem60  40595  fourierdlem42  40684  fourierdlem48  40689  fourierdlem51  40692  fourierdlem54  40695  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem68  40709  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem80  40721  fourierdlem81  40722  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem92  40733  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem100  40741  fourierdlem103  40744  fourierdlem104  40745  fourierdlem105  40746  fourierdlem108  40749  fourierdlem109  40750  fourierdlem110  40751  fourierdlem112  40753  fourierdlem113  40754  sge0pnffigt  40931  sge0resplit  40941  ovnval2  41080  ovnval2b  41087  ovnlecvr  41093  ovnpnfelsup  41094  ovn0lem  41100  ovnsubaddlem1  41105  hoidmvlelem1  41130  ovnhoilem1  41136  ovnhoi  41138  ovnlecvr2  41145  hoiqssbl  41160  ovolval5lem2  41188  ovolval5lem3  41189  ovolval5  41190  ovnovol  41194  smfsuplem2  41339  smfsup  41341  smfinflem  41344  smfinf  41345  cbvrex2  41494  afvelrnb  41564  afvelrnb0  41565  iccelpart  41694  iccpartiun  41695  icceuelpart  41697  cshword2  41762  fmtnofac2lem  41805  fmtnofac2  41806  fmtnofac1  41807  m1expevenALTV  41885  odd2np1ALTV  41910  opoeALTV  41919  opeoALTV  41920  mogoldbblem  41954  isgbow  41965  isgbo  41966  7gbow  41985  9gbo  41987  11gbo  41988  sbgoldbwt  41990  mogoldbb  41998  sbgoldbo  42000  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  bgoldbtbnd  42022  sprsymrelf1lem  42066  sprsymrelf  42070  uspgrsprf1  42080  uspgrsprfo  42081  0nodd  42135  1odd  42136  2nodd  42137  0even  42256  1neven  42257  2even  42258  2zlidl  42259  2zrngamgm  42264  2zrngagrp  42268  2zrngmmgm  42271  2zrngnmrid  42275  lcoval  42526  el0ldep  42580  ldepspr  42587  zlmodzxzldep  42618
  Copyright terms: Public domain W3C validator