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

Theorem rexbii 3037
Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Dec-2019.)
Hypothesis
Ref Expression
rexbii.1 (𝜑𝜓)
Assertion
Ref Expression
rexbii (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)

Proof of Theorem rexbii
StepHypRef Expression
1 rexbii.1 . . 3 (𝜑𝜓)
21anbi2i 729 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3035 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 1988  wrex 2910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-rex 2915
This theorem is referenced by:  2rexbii  3038  rexnal2  3039  ralnex3  3042  r19.29r  3069  r19.29imd  3070  r19.41vv  3086  r19.42v  3087  r19.43  3088  rexcom13  3096  rexrot4  3098  3reeanv  3103  2ralor  3104  cbvrex2v  3175  rexcom4  3220  rexcom4a  3221  rexcom4b  3222  ceqsrex2v  3332  reu7  3395  0el  3931  n0snor2el  4355  uni0b  4454  iuncom  4518  iuncom4  4519  iuniin  4522  dfiunv2  4547  iunab  4557  iunn0  4571  iunin2  4575  iundif2  4578  iunun  4595  iunxiun  4599  iunpwss  4609  inuni  4817  reusv2lem5  4864  reuxfrd  4884  iunopab  5002  dffr2  5069  frc  5070  frminex  5084  dfepfr  5089  epfrc  5090  xpiundi  5163  xpiundir  5164  reliin  5230  iunxpf  5259  cnvuni  5298  dmiun  5322  dfima3  5457  dffr3  5486  rniun  5531  xpdifid  5550  dminxp  5562  imaco  5628  coiun  5633  dffr4  5684  tz6.26  5699  sucel  5786  isarep1  5965  rexrn  6347  ralrn  6348  elrnrexdmb  6350  fnasrn  6396  rexima  6482  ralima  6483  abrexco  6487  imaiun  6488  fliftcnv  6546  rexrnmpt2  6761  iunpw  6963  abrexex2g  7129  abrexex2OLD  7135  el2xptp  7196  rdglem1  7496  tz7.49  7525  oarec  7627  omeu  7650  qsid  7798  eroveu  7827  ixp0  7926  fimax2g  8191  marypha2lem2  8327  dfsup2  8335  infcllem  8378  dfoi  8401  wemapsolem  8440  zfregcl  8484  zfreg  8485  zfregclOLD  8486  zfregOLD  8487  zfreg2OLD  8488  zfregfr  8494  oemapso  8564  zfregs2  8594  infenaleph  8899  isinfcard  8900  kmlem7  8963  kmlem13  8969  fin23lem26  9132  dffin1-5  9195  fin12  9220  numth  9279  ac6n  9292  zorn2lem7  9309  zorng  9311  brdom7disj  9338  brdom6disj  9339  uniwun  9547  axgroth5  9631  axgroth4  9639  grothprim  9641  npomex  9803  genpass  9816  elreal  9937  dfinfre  10989  infrenegsup  10991  uzwo  11736  ublbneg  11758  xrinfmss2  12126  4fvwrd4  12443  fsuppmapnn0fiubex  12775  fsuppmapnn0ub  12778  mptnn0fsuppr  12782  hashge2el2dif  13245  wrdlen1  13326  dfrtrclrec2  13778  rexanuz  14066  rexfiuz  14068  clim0  14218  cbvsum  14406  incexc2  14551  cbvprod  14626  fprodle  14708  iprodmul  14715  divalglem10  15106  divalgb  15108  ncoprmlnprm  15417  phisum  15476  pythagtriplem2  15503  pythagtriplem19  15519  pythagtrip  15520  pceu  15532  prmreclem6  15606  4sqlem12  15641  cshwshashlem1  15783  cshwshash  15792  imasaddfnlem  16169  isdrs2  16920  symgmov1  17793  pmtrprfvalrn  17889  pgpfac1lem5  18459  dvdsrval  18626  opprunit  18642  lsmspsn  19065  lsmelval2  19066  islpidl  19227  mat1dimelbas  20258  mat1dimbas  20259  mdetunilem8  20406  pmatcollpw2lem  20563  tgval2  20741  ntreq0  20862  isclo2  20873  neiptopnei  20917  ist0-3  21130  tgcmp  21185  cmpfi  21192  is1stc2  21226  unisngl  21311  xkobval  21370  txtube  21424  txcmplem1  21425  xkococnlem  21443  eltsms  21917  metrest  22310  iscau3  23057  bcth  23107  pmltpc  23200  itg2i1fseq  23503  itg2cn  23511  plyun0  23934  aaliou3lem9  24086  1cubr  24550  dchrvmasumlema  25170  selbergsb  25245  ostth  25309  istrkg2ld  25340  tglowdim1i  25377  tgdim01  25383  legtrid  25467  midex  25610  ishpg  25632  brbtwn2  25766  colinearalg  25771  ax5seg  25799  axpasch  25802  axlowdimlem6  25808  axeuclidlem  25823  axeuclid  25824  umgr2edg1  26084  umgr2edgneu  26087  nbgrsym  26246  isuvtxa  26276  usgr2pth0  26642  wlkiswwlksupgr2  26744  clwwlksnun  26954  4cycl2vnunb  27134  fusgreg2wsp  27174  lpni  27302  nmobndseqi  27604  hhcmpl  28027  shne0i  28277  nmcopexi  28856  nmcfnexi  28880  cdj3lem3b  29269  rexcom4f  29288  iunin1f  29346  ofpreima  29439  fpwrelmapffslem  29481  tosglblem  29643  xrnarchi  29712  ordtconnlem1  29944  lmdvg  29973  esumfsup  30106  reprsuc  30667  reprdifc  30679  bnj168  30772  bnj1185  30838  bnj1542  30901  bnj865  30967  bnj916  30977  bnj983  30995  bnj1176  31047  bnj1189  31051  bnj1296  31063  bnj1398  31076  bnj1450  31092  bnj1463  31097  cvmliftlem15  31254  cvmlift2lem12  31270  dffr5  31618  imaindm  31656  dfon2lem9  31670  soseq  31725  noseponlem  31791  nosepon  31792  nolt02o  31819  brbigcup  31980  elfuns  31997  brimage  32008  brimg  32019  dfrecs2  32032  imagesset  32035  brub  32036  brsegle  32190  gtinfOLD  32289  filnetlem4  32351  bj-rexcom4a  32845  bj-rexcom4bv  32846  bj-rexcom4b  32847  bj-elsngl  32931  bj-rest10  33016  bj-restreg  33027  bj-mpt2mptALT  33047  iundif1  33354  matunitlindflem1  33376  poimirlem1  33381  poimirlem30  33410  poimirlem32  33412  poimir  33413  ismblfin  33421  volsupnfl  33425  itg2addnclem3  33434  fdc  33512  isfldidl  33838  prtlem10  33969  prter2  33985  islshpat  34123  lshpsmreu  34215  2dim  34575  islpln5  34640  lplnexatN  34668  islvol5  34684  dalem18  34786  dalem20  34798  lhpexle2  35115  lhpexle3  35117  lhpex2leN  35118  4atex2  35182  4atex2-0bOLDN  35184  cdlemftr3  35672  cdlemg17pq  35779  cdlemg19  35791  cdlemg21  35793  cdlemg33d  35816  dva1dim  36092  dih1dimatlem  36437  dihglb2  36450  dvh2dim  36553  mapdrvallem2  36753  mapdpglem3  36783  hdmapglem7a  37038  elrfirn  37077  isnacs2  37088  isnacs3  37092  sbc2rex  37170  4rexfrabdioph  37181  eldioph4b  37194  fphpd  37199  fiphp3d  37202  rencldnfilem  37203  rmxdioph  37402  expdiophlem1  37407  islnm2  37467  elimaint  37759  cnviun  37761  imaiun1  37762  coiun1  37763  elintima  37764  briunov2  37793  clsk3nimkb  38158  prmunb2  38330  zfregs2VD  38896  evth2f  38994  evthf  39006  ndisj2  39038  fnlimabslt  39711  climbddf  39719  limsupub  39736  limsuppnflem  39742  limsupubuz  39745  limsupre2lem  39756  limsupreuz  39769  limsupvaluz2  39770  stoweidlem28  40008  fourierdlem63  40149  fourierdlem65  40151  fourierdlem89  40175  fourierdlem90  40176  fourierdlem91  40177  fourierdlem100  40186  sge0pnfmpt  40425  ovn0  40543  smfaddlem1  40734  smflimlem4  40745  2rexsb  40933  2rexrsb  40934  cbvrex2  40936  2reu5a  40940  copisnmnd  41574  pgrpgt2nabl  41912  islindeps  42007  lindslinindsimp1  42011  lindslinindsimp2  42017  islindeps2  42037  islininds2  42038  isldepslvec2  42039  ldepslinc  42063
  Copyright terms: Public domain W3C validator