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

Theorem rexbidv 3034
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 3031 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wcel 1977  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902
This theorem is referenced by:  2rexbidv  3039  rexralbidv  3040  rexeqbi1dv  3124  rexeqbidv  3130  cbvrex2v  3156  rspc2ev  3295  rspc3ev  3297  ceqsrex2v  3308  uniiunlem  3653  rabasiun  4454  eliun  4455  dfiin2g  4484  dfiunv2  4487  elrnmpt  5280  elrnmptg  5283  elimag  5376  fvelrnb  6138  fvelimab  6148  foelrn  6271  foco2  6272  foco2OLD  6273  elabrex  6383  abrexco  6384  f1oiso  6479  f1oiso2  6480  grprinvlem  6748  orduninsuc  6913  funcnvuni  6990  fun11iun  6997  abrexex2g  7014  abrexex2  7018  f1oweALT  7021  el2xptp  7080  tfrlem12  7350  seqomlem2  7411  nneob  7597  qseq2  7662  elqsg  7663  elqsecl  7666  elixpsn  7811  ixpsnf1o  7812  isfi  7843  enfi  8039  pssnn  8041  frfi  8068  unblem1  8075  unblem2  8076  unbnn2  8080  fofinf1o  8104  finsschain  8134  indexfi  8135  elfi  8180  marypha1lem  8200  supeq3  8216  supmo  8219  suplub  8227  supisolem  8240  eqinf  8251  infval  8253  infglb  8257  infglbb  8258  infmo  8262  oieq1  8278  ordtypelem2  8285  ordtypelem3  8286  ordtypelem9  8292  wemaplem1  8312  brwdom2  8339  brwdom3  8348  unwdomg  8350  oemapval  8441  cantnf  8451  wemapwe  8455  cnfcom3clem  8463  tz9.13  8515  tz9.13g  8516  cardf2  8630  isnum2  8632  ennum  8634  cardiun  8669  infxpenc2  8706  aceq1  8801  aceq2  8803  dfac5lem3  8809  dfac5lem4  8810  dfac2a  8813  dfac2  8814  kmlem9  8841  kmlem12  8844  kmlem14  8846  ackbij1  8921  cflm  8933  cfss  8948  cofsmo  8952  cfsmolem  8953  cfcoflem  8955  coftr  8956  isfin7  8984  fin23lem26  9008  isf32lem5  9040  fin1a2lem11  9093  hsmexlem2  9110  axdc3lem3  9135  axdc3  9137  numthcor  9177  zorn2lem7  9185  brdom3  9209  brdom7disj  9212  brdom6disj  9213  iundom2g  9219  fpwwe2  9322  winainflem  9372  winalim2  9375  inar1  9454  tskuni  9462  nqereu  9608  prnmax  9674  genpv  9678  genpnmax  9686  genpass  9688  prlem936  9726  recexsrlem  9781  map2psrpr  9788  supsrlem  9789  axrrecex  9841  axpre-sup  9847  dedekind  10052  cnegex  10069  recex  10511  fimaxre3  10822  infm3  10834  supaddc  10840  supadd  10841  supmul1  10842  supmullem1  10843  supmullem2  10844  supmul  10845  creur  10864  creui  10865  cju  10866  nnunb  11138  arch  11139  xrsupsslem  11968  xrinfmsslem  11969  xrsupss  11970  xrinfmss  11971  xrub  11973  supxrunb1  11980  supxrunb2  11981  infmremnf  12003  infmrp1  12004  modmuladd  12532  fsequb2  12595  hashge2el2difr  13071  iswrd  13111  wrdval  13112  csbwrdg  13138  cshword  13337  0csh0  13339  2cshwcshw  13371  scshwfzeqfzo  13372  cshimadifsn  13375  shftfval  13607  abs1m  13872  rexfiuz  13884  limsupbnd2  14011  clim  14022  rlim  14023  rlim2  14024  rlim0  14036  rlim0lt  14037  ello1mpt2  14050  o1lo1  14065  o1compt  14115  rlimdiv  14173  climsup  14197  sumeq1  14216  sumeq2w  14219  summo  14244  fsum  14247  fsumcvg3  14256  infcvgaux2i  14378  mertenslem1  14404  mertenslem2  14405  mertens  14406  prodeq1f  14426  prodeq2w  14430  prodmo  14454  fprod  14459  divides  14772  odd2np1lem  14851  opeo  14876  omeo  14877  divalglem4  14906  divalglem10  14912  divalg  14913  gcdcllem3  15010  zeqzmulgcd  15019  bezoutlem1  15043  exprmfct  15203  nnnn0modprm0  15298  pythagtriplem2  15309  pythagtrip  15326  pceu  15338  pcprmpw2  15373  unbenlem  15399  4sqlem12  15447  vdwapval  15464  vdwapun  15465  vdwmc2  15470  vdwpc  15471  vdwlem2  15473  vdwlem10  15481  vdwlem13  15484  vdwnnlem1  15486  rami  15506  cshwsiun  15593  cshwrepswhash1  15596  brssc  16246  isdrs  16706  drsdir  16707  drsdirfi  16710  isdrs2  16711  ipodrsima  16937  gsumvalx  17042  gsumpropd  17044  gsumress  17048  isnsgrp  17060  sgrp2nmndlem5  17188  grpinvex  17204  dfgrp2  17219  grpidinv2  17246  grpidinv  17247  dfgrp3lem  17285  grp1  17294  imasgrp2  17302  conjnmzb  17467  gaorb  17512  orbsta  17518  symgfix2  17608  symgextfo  17614  pmtrprfvalrn  17680  psgnunilem3  17688  psgneu  17698  psgnval  17699  psgnvali  17700  psgnvalii  17701  ispgp  17779  subgpgp  17784  sylow1  17790  pgpfi  17792  sylow2blem3  17809  fislw  17812  sylow3lem2  17815  lsmelvalm  17838  lsmass  17855  pj1fval  17879  pj1val  17880  pj1eu  17881  pj1id  17884  efgrelexlema  17934  efgrelexlemb  17935  efgredeu  17937  cyggeninv  18057  cygabl  18064  pgpfac1lem2  18246  pgpfac1lem3  18248  pgpfac1lem4  18249  pgpfac1  18251  pgpfaclem2  18253  pgpfac  18255  dvdsrval  18417  dvdsr  18418  subrgdvds  18566  lss1d  18733  lspsn  18772  lspsnel  18773  lspsolvlem  18912  rspsn  19024  opsrval  19244  znf1o  19667  cygznlem3  19685  psgndiflemA  19714  ellspd  19908  mat1dimelbas  20044  mat1dimbas  20045  scmatval  20077  scmatel  20078  scmateALT  20085  mat0scmat  20111  decpmataa0  20340  decpmatmulsumfsupp  20345  pmatcollpw2lem  20349  pm2mpmhmlem1  20390  chpscmat  20414  basis2  20514  eltg2  20521  tg2  20528  isclo  20649  neival  20664  isnei  20665  isneip  20667  restbas  20720  neitr  20742  cnpval  20798  iscnp  20799  cnpimaex  20818  lmbr  20820  lmbr2  20821  cnprest2  20852  lmff  20863  regsep  20896  pnrmopn  20905  nrmsep3  20917  isnrm2  20920  iscmp  20949  cmpsublem  20960  cmpsub  20961  tgcmp  20962  sscmp  20966  hauscmplem  20967  1stcclb  21005  1stcfb  21006  is2ndc  21007  2ndc1stc  21012  1stcrest  21014  2ndcctbss  21016  1stcelcls  21022  llyeq  21031  nllyeq  21032  hausllycmp  21055  lly1stc  21057  refssex  21072  refun0  21076  islocfin  21078  locfinnei  21084  comppfsc  21093  txbas  21128  ptval  21131  ptpjopn  21173  ptclsg  21176  txcnp  21181  ptcnp  21183  txrest  21192  ptrescn  21200  txcmp  21204  tx1stc  21211  xkococn  21221  kqreglem1  21302  fbasssin  21398  fbssfi  21399  fbssint  21400  fbun  21402  fgss2  21436  fgcl  21440  ufli  21476  fmfnfmlem3  21518  fbflim2  21539  hauspwpwf1  21549  flfneii  21554  flftg  21558  txflf  21568  fclscf  21587  alexsubb  21608  alexsubALT  21613  tsmssubm  21704  ustincl  21769  ustdiag  21770  ustinvel  21771  ustexhalf  21772  ust0  21781  trust  21791  elutop  21795  ucnval  21839  ucncn  21847  cfiluexsm  21852  cfiluweak  21857  blssps  21987  blss  21988  imasf1oxms  22052  mopni  22055  metss  22071  metrest  22087  metcnp3  22103  cfilucfil  22122  metuel2  22128  nlmvscn  22249  nrginvrcn  22254  icccmplem1  22381  icccmplem2  22382  icccmp  22384  divcn  22427  cncfval  22447  elcncf2  22449  cncfmet  22467  cnheibor  22510  evth  22514  lebnumlem3  22518  lebnum  22519  xlebnum  22520  lebnumii  22521  ipcn  22798  lmmbr  22809  lmmbr2  22810  cfilfval  22815  cfili  22819  iscfil3  22824  caufval  22826  iscau  22827  iscau2  22828  equivcfil  22850  equivcau  22851  lmcau  22864  ovolval  22994  elovolm  22995  ovolgelb  23000  ovoliunlem1  23022  ovoliun2  23026  ovolshftlem1  23029  ovolscalem1  23033  ovolicc  23043  ioombl1lem4  23081  uniioombllem2  23102  mbfaddlem  23178  mbfsup  23182  mbfinf  23183  mbflimsup  23184  i1fmulc  23221  itg1climres  23232  itg2val  23246  itg2l  23247  itg2leub  23252  itg2seq  23260  itg2monolem1  23268  itg2mono  23271  itg2i1fseq2  23274  cniccibl  23358  ellimc3  23394  limciun  23409  dvferm1  23497  dvferm2  23499  lhop1lem  23525  ply1divex  23645  ig1peu  23680  plyval  23698  elply2  23701  coeval  23728  coeeu  23730  coelem  23731  coeeq  23732  plydivlem4  23800  plydivex  23801  aannenlem2  23833  aalioulem2  23837  aaliou2  23844  ulmval  23883  ulm2  23888  ulmcau  23898  ulmdvlem3  23905  abelthlem9  23943  abelth  23944  efif1olem4  24040  eflogeq  24097  efopn  24149  cxpcn3  24234  cxpeq  24243  rlimcnp  24437  lgamgulmlem6  24505  muval  24603  dchrptlem1  24734  dchrptlem2  24735  lgsdchrval  24824  2lgslem1b  24862  pntpbnd  25022  pntibndlem3  25026  pntibnd  25027  pntlemi  25038  pntleme  25042  pntlemp  25044  pnt3  25046  istrkgld  25103  istrkg3ld  25105  axtgsegcon  25108  axtgpasch  25111  axtgcont1  25112  axtgupdim2  25115  legov  25226  islnopp  25377  ishpg  25397  hpgbr  25398  hpgcom  25405  iscgra  25447  iscgra1  25448  isinag  25475  isleag  25479  ttgval  25501  ttgitvval  25508  ttgelitv  25509  brbtwn  25525  brcgr  25526  axpasch  25567  axlowdim2  25586  axlowdim  25587  axcontlem2  25591  axcontlem4  25593  axcontlem7  25596  axcontlem8  25597  nbgraf1olem1  25764  cusgrafilem2  25802  cusgrafi  25804  wwlkn0  26011  clwwlknscsh  26141  erclwwlkneq  26145  eleclclwwlkn  26154  hashecclwwlkn1  26155  usghashecclwwlk  26156  el2wlksot  26201  el2pthsot  26202  2spot2iun2spont  26212  iseupa  26286  3cyclfrgrarn1  26333  usgn0fidegnn0  26350  frgrancvvdeqlem4  26354  friendshipgt3  26442  isgrpo  26529  isgrpoi  26530  grpoidinvlem3  26538  grpoideu  26541  grpoidinv2  26547  nmoofval  26795  nmooval  26796  nmosetn0  26798  nmoolb  26804  nmoubi  26805  nmlno0lem  26826  chcompl  27277  pjhthmo  27339  pjhval  27434  pjpreeq  27435  h1de2ci  27593  elspansn  27603  nmopval  27893  nmopsetn0  27902  nmfnval  27913  nmfnsetn0  27915  eigvecval  27933  hhcno  27941  hhcnf  27942  nmoplb  27944  nmopub  27945  nmfnlb  27961  nmfnleub  27962  eleigvec  27994  nmlnop0iALT  28032  nmopun  28051  nmcexi  28063  branmfn  28142  pjnmopi  28185  cvbr  28319  hatomic  28397  chrelat2  28407  cdjreui  28469  cdj3lem2  28472  reuxfr4d  28508  elabreximd  28526  br8d  28596  unipreima  28620  abfmpunirn  28626  curry2ima  28663  toslublem  28792  tosglblem  28794  archirng  28867  archiexdiv  28869  archiabllem2a  28873  archiabl  28877  isarchiofld  28942  crefi  29036  pcmplfin  29049  pstmfval  29061  tpr2rico  29080  rge0scvg  29117  ismntop  29192  esumc  29234  esumpcvgval  29261  esum2dlem  29275  inelsros  29362  diffiunisros  29363  dya2icoseg2  29461  dya2iocuni  29466  eulerpartlemgvv  29559  eulerpartlemgh  29561  bnj66  29978  bnj873  30042  bnj18eq1  30045  bnj1234  30129  bnj1318  30141  subfacp1lem3  30212  pconcn  30254  cnpcon  30260  txpcon  30262  conpcon  30265  iscvm  30289  cvmcov  30293  cvmopnlem  30308  cvmliftlem15  30328  cvmlift3lem2  30350  cvmlift3lem4  30352  cvmlift3  30358  br8  30693  br6  30694  br4  30695  dfrdg2  30739  dfrdg3  30740  orderseqlem  30787  poseq  30788  soseq  30789  elno  30837  sltval  30838  nobndlem6  30890  nofulllem1  30895  nofulllem2  30896  nofulllem5  30899  altxpeq2  31045  funtransport  31102  fvtransport  31103  brcolinear2  31129  colineardim1  31132  segcon2  31176  brsegle  31179  funray  31211  fvray  31212  funline  31213  linedegen  31214  fvline  31215  ellines  31223  gtinfOLD  31278  nn0prpwlem  31281  fnessref  31316  neibastop2lem  31319  neibastop2  31320  tailfb  31336  unblimceq0lem  31461  unblimceq0  31462  unbdqndv2  31466  bj-finsumval0  32118  relowlssretop  32181  phpreu  32357  matunitlindflem2  32370  ptrest  32372  poimirlem4  32377  poimirlem17  32390  poimirlem20  32393  poimirlem24  32397  poimirlem26  32399  poimirlem27  32400  poimirlem28  32401  poimirlem31  32404  poimirlem32  32405  poimir  32406  heicant  32408  mblfinlem1  32410  mblfinlem3  32412  mblfinlem4  32413  ismblfin  32414  itg2addnclem  32425  itg2addnclem3  32427  itg2addnc  32428  itg2gt0cn  32429  cnicciblnc  32445  ftc1anclem6  32454  unirep  32471  indexa  32492  sdclem2  32502  sdclem1  32503  sdc  32504  fdc  32505  fdc1  32506  incsequz  32508  istotbnd  32532  sstotbnd2  32537  equivtotbnd  32541  isbnd  32543  bndss  32549  ssbnd  32551  totbndbnd  32552  ismtybndlem  32569  heibor1lem  32572  heiborlem1  32574  heiborlem6  32579  heiborlem8  32581  heiborlem10  32583  heibor  32584  rngoid  32665  isgrpda  32718  isdrngo2  32721  divrngidl  32791  prnc  32830  isfldidl  32831  prtlem5  32956  prtlem13  32965  prtlem16  32966  islshp  33078  lsmsat  33107  lcvbr  33120  lsatcv0  33130  lshpsmreu  33208  lshpkrlem1  33209  lshpkrlem2  33210  lshpkrlem3  33211  lshpkrcl  33215  lshpset2N  33218  islshpkrN  33219  cvrval  33368  atlex  33415  glbconxN  33476  hlsuprexch  33479  islln  33604  islpln  33628  islpln5  33633  lvolex3N  33636  islvol  33671  islvol5  33677  ispointN  33840  pmapglbx  33867  paddval  33896  elpaddn0  33898  elpaddat  33902  elpadd0  33907  4atex  34174  4atex2  34175  cdlemefrs29bpre1  34497  cdlemefrs32fva  34500  cdlemg33b  34807  dvhb1dimN  35086  dvhopellsm  35218  dib1dim  35266  diclspsn  35295  dihglblem2aN  35394  dihglblem2N  35395  dih1dimatlem  35430  dvh3dimatN  35540  dvh2dim  35546  dvh3dim  35547  dvh4dimN  35548  dvh3dim3N  35550  dochfl1  35577  lcfl7N  35602  lcf1o  35652  lcfrlem39  35682  mapdpglem3  35776  hvmapvalvalN  35862  hdmap14lem2a  35971  hdmapglem7a  36031  elrfi  36069  isnacs  36079  nacsfg  36080  nacsfix  36087  mzpcompact2lem  36126  eldiophb  36132  eldioph  36133  eldioph2  36137  eldioph2b  36138  eldioph3  36141  eldiophss  36150  diophrex  36151  sbcrexgOLD  36161  sbc2rexgOLD  36164  rexrabdioph  36170  rexfrabdioph  36171  elnn0rabdioph  36179  dvdsrabdioph  36186  eldioph4b  36187  eldioph4i  36188  diophren  36189  rencldnfilem  36196  pell1234qrdich  36237  jm2.27  36387  expdiophlem1  36400  wepwsolem  36424  aomclem8  36443  islnr3  36498  lnr2i  36499  lpirlnr  36500  hbtlem1  36506  hbtlem2  36507  hbtlem7  36508  hbtlem4  36509  hbtlem5  36511  hbtlem6  36512  dgraaval  36527  dgraalem  36528  dgraaub  36531  rngunsnply  36556  brtrclfv2  36832  clsk1indlem1  37157  extoimad  37280  elabrexg  38023  foelrnf  38162  disjrnmpt2  38164  upbdrech  38254  ssfiunibd  38258  supxrgere  38284  supxrgelem  38288  supxrge  38289  suplesup  38290  infxr  38318  infleinf  38323  iccshift  38385  iooshift  38389  climinf  38467  climinff  38472  ellimcabssub0  38478  climf  38483  limcperiod  38489  limclner  38512  climf2  38527  clim2d  38534  cncfshiftioo  38572  fperdvper  38602  itgiccshift  38666  itgperiod  38667  stoweidlem27  38714  stoweidlem31  38718  stoweidlem43  38730  stoweidlem46  38733  stoweidlem52  38739  stoweidlem60  38747  fourierdlem42  38836  fourierdlem48  38841  fourierdlem51  38844  fourierdlem54  38847  fourierdlem63  38856  fourierdlem64  38857  fourierdlem65  38858  fourierdlem68  38861  fourierdlem70  38863  fourierdlem71  38864  fourierdlem73  38866  fourierdlem80  38873  fourierdlem81  38874  fourierdlem89  38882  fourierdlem90  38883  fourierdlem91  38884  fourierdlem92  38885  fourierdlem96  38889  fourierdlem97  38890  fourierdlem98  38891  fourierdlem99  38892  fourierdlem100  38893  fourierdlem103  38896  fourierdlem104  38897  fourierdlem105  38898  fourierdlem108  38901  fourierdlem109  38902  fourierdlem110  38903  fourierdlem112  38905  fourierdlem113  38906  sge0pnffigt  39083  sge0resplit  39093  ovnval2  39229  ovnval2b  39236  ovnlecvr  39242  ovnpnfelsup  39243  ovn0lem  39249  ovnsubaddlem1  39254  hoidmvlelem1  39279  ovnhoilem1  39285  ovnhoi  39287  ovnlecvr2  39294  hoiqssbl  39309  ovolval5lem2  39337  ovolval5lem3  39338  ovolval5  39339  ovnovol  39343  cbvrex2  39616  afvelrnb  39687  afvelrnb0  39688  iccelpart  39766  iccpartiun  39767  icceuelpart  39769  fmtnofac2lem  39813  fmtnofac2  39814  fmtnofac1  39815  m1expevenALTV  39893  odd2np1ALTV  39918  opoeALTV  39927  opeoALTV  39928  isgbo  39969  isgboa  39970  7gbo  39989  9gboa  39991  11gboa  39992  bgoldbwt  39994  nnsum3primesgbe  40003  nnsum4primesodd  40007  nnsum4primesoddALTV  40008  bgoldbtbnd  40020  cshword2  40095  n0snor2el  40113  upgredg2vtx  40365  usgredg4  40436  ushgredgedga  40448  ushgredgedgaloop  40450  dfnbgr2  40553  nbgrel  40556  nbumgrvtx  40560  nbgrnself  40575  uvtxael1  40614  uvtxa01vtx0  40615  cusgrfilem2  40664  cusgrfi  40666  vtxd0nedgb  40695  fusgrn0degnn0  40706  wlkOnl1iedg  40865  wspniunwspnon  41122  elwwlks2on  41154  clwwlksnscsh  41239  erclwwlksneq  41243  eleclclwwlksn  41252  hashecclwwlksn1  41253  umgrhashecclwwlk  41254  3cyclfrgrrn1  41447  frgrncvvdeqlem4  41464  av-friendshipgt3  41544  0nodd  41592  1odd  41593  2nodd  41594  0even  41713  1neven  41714  2even  41715  2zlidl  41716  2zrngamgm  41721  2zrngagrp  41725  2zrngmmgm  41728  2zrngnmrid  41732  lcoval  41987  el0ldep  42041  ldepspr  42048  zlmodzxzldep  42079
  Copyright terms: Public domain W3C validator