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

Theorem rexbidv 3240
Description: Formula-building rule for restricted existential quantifier (deduction form). (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 468 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexbidva 3237 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wcel 2156  wrex 3097
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
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-rex 3102
This theorem is referenced by:  2rexbidv  3245  rexralbidv  3246  rexeqbi1dv  3336  rexeqbidv  3342  cbvrex2v  3369  rspc2ev  3517  rspc3ev  3519  ceqsrex2v  3532  uniiunlem  3889  n0snor2el  4552  eliun  4716  dfiin2g  4745  dfiunv2  4748  elrnmpt  5573  elrnmptg  5576  elimag  5680  fvelrnb  6460  fvelimab  6470  foelrn  6596  foco2  6597  elabrex  6721  abrexco  6722  f1oiso  6821  f1oiso2  6822  grprinvlem  7098  orduninsuc  7269  funcnvuni  7345  fun11iun  7352  abrexex2g  7370  abrexex2OLD  7376  f1oweALT  7378  el2xptp  7439  tfrlem12  7717  seqomlem2  7778  nneob  7965  qseq2  8028  elqsg  8029  elqsecl  8032  elixpsn  8180  ixpsnf1o  8181  isfi  8212  enfi  8411  pssnn  8413  frfi  8440  unblem1  8447  unblem2  8448  unbnn2  8452  fofinf1o  8476  finsschain  8508  indexfi  8509  elfi  8554  marypha1lem  8574  supeq3  8590  supmo  8593  suplub  8601  supisolem  8614  eqinf  8625  infval  8627  infglb  8631  infglbb  8632  infmo  8636  oieq1  8652  ordtypelem2  8659  ordtypelem3  8660  ordtypelem9  8666  wemaplem1  8686  brwdom2  8713  brwdom3  8722  unwdomg  8724  oemapval  8823  cantnf  8833  wemapwe  8837  cnfcom3clem  8845  tz9.13  8897  tz9.13g  8898  cardf2  9048  isnum2  9050  ennum  9052  cardiun  9087  infxpenc2  9124  aceq1  9219  aceq2  9221  dfac5lem3  9227  dfac5lem4  9228  dfac2a  9231  dfac2b  9232  dfac2OLD  9234  kmlem9  9261  kmlem12  9264  kmlem14  9266  ackbij1  9341  cflm  9353  cfss  9368  cofsmo  9372  cfsmolem  9373  cfcoflem  9375  coftr  9376  isfin7  9404  fin23lem26  9428  isf32lem5  9460  fin1a2lem11  9513  hsmexlem2  9530  axdc3lem3  9555  axdc3  9557  numthcor  9597  zorn2lem7  9605  brdom3  9631  brdom7disj  9634  brdom6disj  9635  iundom2g  9643  fpwwe2  9746  winainflem  9796  winalim2  9799  inar1  9878  tskuni  9886  nqereu  10032  prnmax  10098  genpv  10102  genpnmax  10110  genpass  10112  prlem936  10150  recexsrlem  10205  map2psrpr  10212  supsrlem  10213  axrrecex  10265  axpre-sup  10271  dedekind  10481  cnegex  10498  recex  10940  fimaxre3  11251  infm3  11263  supaddc  11271  supadd  11272  supmul1  11273  supmullem1  11274  supmullem2  11275  supmul  11276  creur  11295  creui  11296  cju  11297  nnunb  11551  arch  11552  xrsupsslem  12351  xrinfmsslem  12352  xrsupss  12353  xrinfmss  12354  xrub  12356  supxrunb1  12363  supxrunb2  12364  infmremnf  12387  infmrp1  12388  modmuladd  12932  fsequb2  12995  hashge2el2difr  13476  iswrd  13514  wrdval  13515  csbwrdg  13541  cshword  13757  0csh0  13759  2cshwcshw  13791  scshwfzeqfzo  13792  cshimadifsn  13795  shftfval  14029  abs1m  14294  rexfiuz  14306  limsupbnd2  14433  clim  14444  rlim  14445  rlim2  14446  rlim0  14458  rlim0lt  14459  ello1mpt2  14472  o1lo1  14487  o1compt  14537  rlimdiv  14595  climsup  14619  sumeq1  14638  sumeq2w  14641  summo  14667  fsum  14670  fsumcvg3  14679  infcvgaux2i  14808  mertenslem1  14833  mertenslem2  14834  mertens  14835  prodeq1f  14855  prodeq2w  14859  prodmo  14883  fprod  14888  divides  15201  odd2np1lem  15280  opeo  15305  omeo  15306  divalglem4  15335  divalglem10  15341  divalg  15342  gcdcllem3  15438  zeqzmulgcd  15447  bezoutlem1  15471  exprmfct  15629  nnnn0modprm0  15724  pythagtriplem2  15735  pythagtrip  15752  pceu  15764  pcprmpw2  15799  unbenlem  15825  4sqlem12  15873  vdwapval  15890  vdwapun  15891  vdwmc2  15896  vdwpc  15897  vdwlem2  15899  vdwlem10  15907  vdwlem13  15910  vdwnnlem1  15912  rami  15932  cshwsiun  16014  cshwrepswhash1  16017  brssc  16674  isdrs  17135  drsdir  17136  drsdirfi  17139  isdrs2  17140  ipodrsima  17366  gsumvalx  17471  gsumpropd  17473  gsumress  17477  isnsgrp  17489  sgrp2nmndlem5  17617  grpinvex  17633  dfgrp2  17648  grpidinv2  17675  grpidinv  17676  dfgrp3lem  17714  grp1  17723  imasgrp2  17731  conjnmzb  17893  gaorb  17937  orbsta  17943  symgfix2  18033  symgextfo  18039  pmtrprfvalrn  18105  psgnunilem3  18113  psgneu  18123  psgnval  18124  psgnvali  18125  psgnvalii  18126  ispgp  18204  subgpgp  18209  sylow1  18215  pgpfi  18217  sylow2blem3  18234  fislw  18237  sylow3lem2  18240  lsmelvalm  18263  lsmass  18280  pj1fval  18304  pj1val  18305  pj1eu  18306  pj1id  18309  efgrelexlema  18359  efgrelexlemb  18360  efgredeu  18362  cyggeninv  18482  cygabl  18489  pgpfac1lem2  18672  pgpfac1lem3  18674  pgpfac1lem4  18675  pgpfac1  18677  pgpfaclem2  18679  pgpfac  18681  dvdsrval  18843  dvdsr  18844  subrgdvds  18994  lss1d  19166  lspsn  19205  lspsnel  19206  lspsolvlem  19346  rspsn  19459  opsrval  19679  znf1o  20103  cygznlem3  20121  psgndiflemA  20151  ellspd  20347  mat1dimelbas  20484  mat1dimbas  20485  scmatval  20517  scmatel  20518  scmateALT  20525  mat0scmat  20551  decpmataa0  20782  decpmatmulsumfsupp  20787  pmatcollpw2lem  20791  pm2mpmhmlem1  20832  chpscmat  20856  basis2  20965  eltg2  20972  tg2  20979  isclo  21101  neival  21116  isnei  21117  isneip  21119  restbas  21172  neitr  21194  cnpval  21250  iscnp  21251  cnpimaex  21270  lmbr  21272  lmbr2  21273  cnprest2  21304  lmff  21315  regsep  21348  pnrmopn  21357  nrmsep3  21369  isnrm2  21372  iscmp  21401  cmpsublem  21412  cmpsub  21413  tgcmp  21414  sscmp  21418  hauscmplem  21419  1stcclb  21457  1stcfb  21458  is2ndc  21459  2ndc1stc  21464  1stcrest  21466  2ndcctbss  21468  1stcelcls  21474  llyeq  21483  nllyeq  21484  hausllycmp  21507  lly1stc  21509  refssex  21524  refun0  21528  islocfin  21530  locfinnei  21536  comppfsc  21545  txbas  21580  ptval  21583  ptpjopn  21625  ptclsg  21628  txcnp  21633  ptcnp  21635  txrest  21644  ptrescn  21652  txcmp  21656  tx1stc  21663  xkococn  21673  kqreglem1  21754  fbasssin  21849  fbssfi  21850  fbssint  21851  fbun  21853  fgss2  21887  fgcl  21891  ufli  21927  fmfnfmlem3  21969  fbflim2  21990  hauspwpwf1  22000  flfneii  22005  flftg  22009  txflf  22019  fclscf  22038  alexsubb  22059  alexsubALT  22064  tsmssubm  22155  ustincl  22220  ustdiag  22221  ustinvel  22222  ustexhalf  22223  ust0  22232  trust  22242  elutop  22246  ucnval  22290  ucncn  22298  cfiluexsm  22303  cfiluweak  22308  blssps  22438  blss  22439  imasf1oxms  22503  mopni  22506  metss  22522  metrest  22538  metcnp3  22554  cfilucfil  22573  metuel2  22579  nlmvscn  22700  nrginvrcn  22705  icccmplem1  22834  icccmplem2  22835  icccmp  22837  divcn  22880  cncfval  22900  elcncf2  22902  cncfmet  22920  cnheibor  22963  evth  22967  lebnumlem3  22971  lebnum  22972  xlebnum  22973  lebnumii  22974  ipcn  23253  lmmbr  23264  lmmbr2  23265  cfilfval  23270  cfili  23274  iscfil3  23279  caufval  23281  iscau  23282  iscau2  23283  equivcfil  23305  equivcau  23306  lmcau  23319  ovolval  23450  elovolm  23452  ovolgelb  23457  ovoliunlem1  23479  ovoliun2  23483  ovolshftlem1  23486  ovolscalem1  23490  ovolicc  23500  ioombl1lem4  23538  uniioombllem2  23560  mbfaddlem  23637  mbfsup  23641  mbfinf  23642  mbflimsup  23643  i1fmulc  23680  itg1climres  23691  itg2val  23705  itg2l  23706  itg2leub  23711  itg2seq  23719  itg2monolem1  23727  itg2mono  23730  itg2i1fseq2  23733  cniccibl  23817  ellimc3  23853  limciun  23868  dvferm1  23958  dvferm2  23960  lhop1lem  23986  ply1divex  24106  ig1peu  24141  plyval  24159  elply2  24162  coeval  24189  coeeu  24191  coelem  24192  coeeq  24193  plydivlem4  24261  plydivex  24262  aannenlem2  24294  aalioulem2  24298  aaliou2  24305  ulmval  24344  ulm2  24349  ulmcau  24359  ulmdvlem3  24366  abelthlem9  24404  abelth  24405  efif1olem4  24502  eflogeq  24558  efopn  24614  cxpcn3  24699  cxpeq  24708  rlimcnp  24902  lgamgulmlem6  24970  muval  25068  dchrptlem1  25199  dchrptlem2  25200  lgsdchrval  25289  2lgslem1b  25327  pntpbnd  25487  pntibndlem3  25491  pntibnd  25492  pntlemi  25503  pntleme  25507  pntlemp  25509  pnt3  25511  istrkgld  25568  istrkg3ld  25570  axtgsegcon  25573  axtgpasch  25576  axtgcont1  25577  axtgupdim2  25580  legov  25690  islnopp  25841  ishpg  25861  hpgbr  25862  hpgcom  25869  iscgra  25911  iscgra1  25912  isinag  25939  isleag  25943  ttgval  25965  ttgitvval  25972  ttgelitv  25973  brbtwn  25989  brcgr  25990  axpasch  26031  axlowdim2  26050  axlowdim  26051  axcontlem2  26055  axcontlem4  26057  axcontlem7  26060  axcontlem8  26061  upgredg2vtx  26247  edglnl  26249  usgredg4  26320  ushgredgedg  26332  ushgredgedgloop  26334  ushgredgedgloopOLD  26335  dfnbgr2  26442  nbgrel  26445  nbgrelOLD  26446  nbumgrvtx  26454  nbgrnself  26467  uvtxel1  26513  uvtxael1OLD  26515  uvtxa01vtx0OLD  26516  cusgrfilem2  26576  cusgrfi  26578  vtxd0nedgb  26608  fusgrn0degnn0  26619  wlkonl1iedg  26785  wspniunwspnon  27059  elwwlks2on  27096  clwwlknscsh  27209  erclwwlkneq  27214  eleclclwwlkn  27223  hashecclwwlkn1  27224  umgrhashecclwwlk  27225  3cyclfrgrrn1  27456  friendshipgt3  27582  isgrpo  27676  isgrpoi  27677  grpoidinvlem3  27685  grpoideu  27688  grpoidinv2  27694  nmoofval  27941  nmooval  27942  nmosetn0  27944  nmoolb  27950  nmoubi  27951  nmlno0lem  27972  chcompl  28423  pjhthmo  28485  pjhval  28580  pjpreeq  28581  h1de2ci  28739  elspansn  28749  nmopval  29039  nmopsetn0  29048  nmfnval  29059  nmfnsetn0  29061  eigvecval  29079  hhcno  29087  hhcnf  29088  nmoplb  29090  nmopub  29091  nmfnlb  29107  nmfnleub  29108  eleigvec  29140  nmlnop0iALT  29178  nmopun  29197  nmcexi  29209  branmfn  29288  pjnmopi  29331  cvbr  29465  hatomic  29543  chrelat2  29553  cdjreui  29615  cdj3lem2  29618  reuxfr4d  29652  elabreximd  29669  br8d  29743  unipreima  29769  abfmpunirn  29775  curry2ima  29809  toslublem  29988  tosglblem  29990  archirng  30063  archiexdiv  30065  archiabllem2a  30069  archiabl  30073  isarchiofld  30138  crefi  30235  pcmplfin  30248  pstmfval  30260  tpr2rico  30279  rge0scvg  30316  ismntop  30391  esumc  30434  esumpcvgval  30461  esum2dlem  30475  inelsros  30562  diffiunisros  30563  dya2icoseg2  30661  dya2iocuni  30666  eulerpartlemgvv  30759  eulerpartlemgh  30761  hgt749d  31048  tgoldbachgt  31062  bnj66  31248  bnj873  31312  bnj18eq1  31315  bnj1234  31399  bnj1318  31411  subfacp1lem3  31482  pconncn  31524  cnpconn  31530  txpconn  31532  connpconn  31535  iscvm  31559  cvmcov  31563  cvmopnlem  31578  cvmliftlem15  31598  cvmlift3lem2  31620  cvmlift3lem4  31622  cvmlift3  31628  br8  31963  br6  31964  br4  31965  dfrdg2  32016  dfrdg3  32017  orderseqlem  32068  poseq  32069  soseq  32070  elno  32115  sltval  32116  noprefixmo  32164  nosupno  32165  nosupdm  32166  nosupfv  32168  nosupres  32169  nosupbnd1lem1  32170  nosupbnd1lem3  32172  nosupbnd1lem4  32173  nosupbnd1lem5  32174  noeta  32184  altxpeq2  32397  funtransport  32454  fvtransport  32455  brcolinear2  32481  colineardim1  32484  segcon2  32528  brsegle  32531  funray  32563  fvray  32564  funline  32565  linedegen  32566  fvline  32567  ellines  32575  gtinfOLD  32630  nn0prpwlem  32633  fnessref  32668  neibastop2lem  32671  neibastop2  32672  tailfb  32688  unblimceq0lem  32809  unblimceq0  32810  unbdqndv2  32814  bj-finsumval0  33459  relowlssretop  33522  cnfinltrel  33552  phpreu  33701  matunitlindflem2  33714  ptrest  33716  poimirlem4  33721  poimirlem17  33734  poimirlem20  33737  poimirlem24  33741  poimirlem26  33743  poimirlem27  33744  poimirlem28  33745  poimirlem31  33748  poimirlem32  33749  poimir  33750  heicant  33752  mblfinlem1  33754  mblfinlem3  33756  mblfinlem4  33757  ismblfin  33758  itg2addnclem  33768  itg2addnclem3  33770  itg2addnc  33771  itg2gt0cn  33772  cnicciblnc  33788  ftc1anclem6  33797  unirep  33814  indexa  33835  sdclem2  33844  sdclem1  33845  sdc  33846  fdc  33847  fdc1  33848  incsequz  33850  istotbnd  33874  sstotbnd2  33879  equivtotbnd  33883  isbnd  33885  bndss  33891  ssbnd  33893  totbndbnd  33894  ismtybndlem  33911  heibor1lem  33914  heiborlem1  33916  heiborlem6  33921  heiborlem8  33923  heiborlem10  33925  heibor  33926  rngoid  34007  isgrpda  34060  isdrngo2  34063  divrngidl  34133  prnc  34172  isfldidl  34173  exanres3  34376  brcoels  34498  br1cossxrnres  34506  eldm1cossres2  34519  prtlem5  34634  prtlem13  34642  prtlem16  34643  islshp  34754  lsmsat  34783  lcvbr  34796  lsatcv0  34806  lshpsmreu  34884  lshpkrlem1  34885  lshpkrlem2  34886  lshpkrlem3  34887  lshpkrcl  34891  lshpset2N  34894  islshpkrN  34895  cvrval  35044  atlex  35091  glbconxN  35153  hlsuprexch  35156  islln  35281  islpln  35305  islpln5  35310  lvolex3N  35313  islvol  35348  islvol5  35354  ispointN  35517  pmapglbx  35544  paddval  35573  elpaddn0  35575  elpaddat  35579  elpadd0  35584  4atex  35851  4atex2  35852  cdlemefrs29bpre1  36172  cdlemefrs32fva  36175  cdlemg33b  36482  dvhb1dimN  36761  dvhopellsm  36892  dib1dim  36940  diclspsn  36969  dihglblem2aN  37068  dihglblem2N  37069  dih1dimatlem  37104  dvh3dimatN  37214  dvh2dim  37220  dvh3dim  37221  dvh4dimN  37222  dvh3dim3N  37224  dochfl1  37251  lcfl7N  37276  lcf1o  37326  lcfrlem39  37356  mapdpglem3  37450  hvmapvalvalN  37536  hdmap14lem2a  37642  hdmapglem7a  37702  elrfi  37753  isnacs  37763  nacsfg  37764  nacsfix  37771  mzpcompact2lem  37810  eldiophb  37816  eldioph  37817  eldioph2  37821  eldioph2b  37822  eldioph3  37825  eldiophss  37834  diophrex  37835  sbcrexgOLD  37845  sbc2rexgOLD  37848  rexrabdioph  37854  rexfrabdioph  37855  elnn0rabdioph  37863  dvdsrabdioph  37870  eldioph4b  37871  eldioph4i  37872  diophren  37873  rencldnfilem  37880  pell1234qrdich  37921  jm2.27  38070  expdiophlem1  38083  wepwsolem  38107  aomclem8  38126  islnr3  38180  lnr2i  38181  lpirlnr  38182  hbtlem1  38188  hbtlem2  38189  hbtlem7  38190  hbtlem4  38191  hbtlem5  38193  hbtlem6  38194  dgraaval  38209  dgraalem  38210  dgraaub  38213  rngunsnply  38238  brtrclfv2  38513  clsk1indlem1  38837  extoimad  38958  elabrexg  39694  foelrnf  39856  disjrnmpt2  39858  upbdrech  39994  ssfiunibd  39998  supxrgere  40023  supxrgelem  40027  supxrge  40028  suplesup  40029  infxr  40057  infleinf  40062  supxrunb3  40096  unb2ltle  40115  uzub  40131  supminfxr  40167  iccshift  40219  iooshift  40223  climinf  40312  climinff  40317  ellimcabssub0  40323  climf  40328  limcperiod  40334  limclner  40357  climf2  40372  clim2d  40379  limsupref  40391  limsuppnfd  40408  limsuppnf  40417  climinfmpt  40421  limsupubuzmpt  40425  limsupmnf  40427  limsupre2lem  40430  limsupre2  40431  limsupmnfuz  40433  limsupre2mpt  40436  limsupre3lem  40438  limsupre3  40439  limsupre3mpt  40440  limsupre3uzlem  40441  limsupre3uz  40442  limsupreuz  40443  limsupreuzmpt  40445  climuz  40450  liminfreuzlem  40508  liminfreuz  40509  xlimmnfvlem1  40532  xlimmnfv  40534  xlimpnfvlem1  40536  xlimpnfv  40538  cncfshiftioo  40579  fperdvper  40607  itgiccshift  40669  itgperiod  40670  stoweidlem27  40717  stoweidlem31  40721  stoweidlem43  40733  stoweidlem46  40736  stoweidlem52  40742  stoweidlem60  40750  fourierdlem42  40839  fourierdlem48  40844  fourierdlem51  40847  fourierdlem54  40850  fourierdlem63  40859  fourierdlem64  40860  fourierdlem65  40861  fourierdlem68  40864  fourierdlem70  40866  fourierdlem71  40867  fourierdlem73  40869  fourierdlem80  40876  fourierdlem81  40877  fourierdlem89  40885  fourierdlem90  40886  fourierdlem91  40887  fourierdlem92  40888  fourierdlem96  40892  fourierdlem97  40893  fourierdlem98  40894  fourierdlem99  40895  fourierdlem100  40896  fourierdlem103  40899  fourierdlem104  40900  fourierdlem105  40901  fourierdlem108  40904  fourierdlem109  40905  fourierdlem110  40906  fourierdlem112  40908  fourierdlem113  40909  sge0pnffigt  41086  sge0resplit  41096  ovnval2  41235  ovnval2b  41242  ovnlecvr  41248  ovnpnfelsup  41249  ovn0lem  41255  ovnsubaddlem1  41260  hoidmvlelem1  41285  ovnhoilem1  41291  ovnhoi  41293  ovnlecvr2  41300  hoiqssbl  41315  ovolval5lem2  41343  ovolval5lem3  41344  ovolval5  41345  ovnovol  41349  smfsuplem2  41494  smfsup  41496  smfinflem  41499  smfinf  41500  cbvrex2  41680  afvelrnb  41746  afvelrnb0  41747  iccelpart  41938  iccpartiun  41939  icceuelpart  41941  cshword2  42006  fmtnofac2lem  42049  fmtnofac2  42050  fmtnofac1  42051  m1expevenALTV  42129  odd2np1ALTV  42154  opoeALTV  42163  opeoALTV  42164  mogoldbblem  42198  isgbow  42209  isgbo  42210  7gbow  42229  9gbo  42231  11gbo  42232  sbgoldbwt  42234  mogoldbb  42242  sbgoldbo  42244  nnsum3primesgbe  42249  nnsum4primesodd  42253  nnsum4primesoddALTV  42254  bgoldbtbnd  42266  sprsymrelf1lem  42303  sprsymrelf  42307  uspgrsprf1  42317  uspgrsprfo  42318  0nodd  42372  1odd  42373  2nodd  42374  0even  42493  1neven  42494  2even  42495  2zlidl  42496  2zrngamgm  42501  2zrngagrp  42505  2zrngmmgm  42508  2zrngnmrid  42512  lcoval  42763  el0ldep  42817  ldepspr  42824  zlmodzxzldep  42855
  Copyright terms: Public domain W3C validator