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

Theorem rexbii 2959
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 694 . 2
32rexbii2 2957 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  2rexbii  2960  rexnal2  2961  rexanaliOLD  2962  r19.29r  2993  r19.29imd  2994  r19.41vv  3011  r19.42v  3012  r19.43  3013  rexcom13  3020  rexrot4  3021  3reeanv  3026  2ralor  3027  cbvrex2v  3093  rexcom4  3129  rexcom4a  3130  rexcom4b  3131  ceqsrex2v  3235  reu7  3294  0el  3802  uni0b  4274  rabasiun  4334  iuncom  4337  iuncom4  4338  iuniin  4341  dfiunv2  4366  iunab  4376  iunn0  4390  iunin2  4394  iundif2  4397  iunun  4411  iunxiun  4413  iunpwss  4420  inuni  4614  reusv2lem5  4657  reusv5OLD  4662  reusv7OLD  4664  reuxfrd  4677  iunopab  4788  dffr2  4849  frc  4850  frminex  4864  dfepfr  4869  epfrc  4870  sucel  4956  xpiundi  5059  xpiundir  5060  reliin  5129  iunxpf  5156  cnvuni  5194  dmiun  5216  dfima3  5345  dffr3  5374  rniun  5421  xpdifid  5440  dminxp  5452  imaco  5517  coiun  5522  isarep1  5672  rexrn  6033  ralrn  6034  elrnrexdmb  6036  fnasrn  6077  rexima  6151  ralima  6152  abrexco  6156  imaiun  6157  fliftcnv  6209  rexrnmpt2  6418  iunpw  6614  abrexex2g  6777  abrexex2  6781  el2xptp  6843  rdglem1  7100  tz7.49  7129  oarec  7230  omeu  7253  qsid  7396  eroveu  7425  ixp0  7522  fimax2g  7786  marypha2lem2  7916  dfsup2  7922  dfsup2OLD  7923  dfoi  7957  wemapsolem  7996  zfregcl  8041  zfreg  8042  zfreg2  8043  oemapso  8122  zfregs2  8185  infenaleph  8493  isinfcard  8494  kmlem7  8557  kmlem13  8563  fin23lem26  8726  dffin1-5  8789  fin12  8814  numth  8873  ac6n  8886  zorn2lem7  8903  zorng  8905  brdom7disj  8930  brdom6disj  8931  uniwun  9139  axgroth5  9223  axgroth4  9231  grothprim  9233  npomex  9395  genpass  9408  elreal  9529  dfinfmr  10545  infmsup  10546  infmrgelb  10548  infmrlb  10549  uzwo  11173  uzwoOLD  11174  ublbneg  11195  xrinfmss2  11531  4fvwrd4  11822  fsuppmapnn0fiubex  12098  fsuppmapnn0ub  12101  mptnn0fsuppr  12105  hashge2el2dif  12521  wrdlen1  12579  rexanuz  13178  rexfiuz  13180  clim0  13329  cbvsum  13517  incexc2  13650  cbvprod  13722  iprodmul  13796  divalglem10  14060  divalgb  14062  pythagtriplem2  14341  pythagtriplem19  14357  pythagtrip  14358  pceu  14370  prmreclem6  14439  4sqlem12  14474  cshwshashlem1  14580  cshwshash  14589  imasaddfnlem  14925  isdrs2  15568  symgmov1  16417  pmtrprfvalrn  16513  pgpfac1lem5  17130  dvdsrval  17294  opprunit  17310  lsmspsn  17730  lsmelval2  17731  islpidl  17894  mat1dimelbas  18973  mat1dimbas  18974  mdetunilem8  19121  pmatcollpw2lem  19278  tgval2  19457  ntreq0  19578  isclo2  19589  neiptopnei  19633  ist0-3  19846  tgcmp  19901  cmpfi  19908  is1stc2  19943  unisngl  20028  xkobval  20087  txtube  20141  txcmplem1  20142  xkococnlem  20160  eltsms  20631  metrest  21027  iscau3  21717  bcth  21768  pmltpc  21862  itg2i1fseq  22162  itg2cn  22170  plyun0  22594  aaliou3lem9  22746  1cubr  23173  dchrvmasumlema  23685  selbergsb  23760  ostth  23824  istrkg2ld  23858  tglowdim1i  23892  tgdim01  23898  legtrid  23978  midex  24111  brbtwn2  24208  colinearalg  24213  ax5seg  24241  axpasch  24244  axlowdimlem6  24250  axeuclidlem  24265  axeuclid  24266  usgra2edg1  24383  nbgraop1  24425  nbgraf1olem1  24441  el2wlkonot  24869  el2spthonot  24870  el2wlkonotot0  24872  4cycl2vnunb  25017  vdn0frgrav2  25023  vdgn0frgrav2  25024  usg2spot2nb  25065  usgreg2spot  25067  numclwwlkun  25079  lpni  25181  isgrpo2  25199  isgrp2d  25237  nmobndseqi  25694  hhcmpl  26117  shne0i  26366  nmcopexi  26946  nmcfnexi  26970  cdj3lem3b  27359  rexcom4f  27376  disjunsn  27453  ofpreima  27507  fpwrelmapffslem  27555  tosglblem  27657  xrnarchi  27728  ordtconlem1  27906  lmdvg  27935  esumfsup  28076  cvmliftlem15  28743  cvmlift2lem12  28759  dfrtrclrec2  29066  dffr5  29182  dfon2lem9  29223  dffr4  29262  tz6.26  29285  soseq  29334  nodenselem4  29444  nodenselem5  29445  nofulllem5  29466  brbigcup  29548  elfuns  29565  brimage  29576  brimg  29587  tfrqfree  29601  imagesset  29603  brub  29604  brsegle  29758  iundif1  30037  ismblfin  30055  volsupnfl  30059  itg2addnclem3  30068  gtinf  30137  filnetlem4  30199  fdc  30238  isfldidl  30465  prtlem10  30606  prter2  30622  elrfirn  30627  isnacs2  30638  isnacs3  30642  sbc2rex  30720  4rexfrabdioph  30731  eldioph4b  30745  fphpd  30750  fiphp3d  30753  rencldnfilem  30754  rmxdioph  30958  expdiophlem1  30963  islnm2  31024  phisum  31159  prmunb2  31191  evth2f  31390  evthf  31402  fprodle  31604  stoweidlem28  31810  fourierdlem63  31952  fourierdlem65  31954  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem100  31989  2rexsb  32175  2rexrsb  32176  cbvrex2  32178  2reu5a  32182  usgra2pth0  32355  usgvincvad  32404  usgvincvadALT  32407  usg2edgneu  32412  copisnmnd  32497  pgrpgt2nabl  32959  islindeps  33054  lindslinindsimp1  33058  lindslinindsimp2  33064  islindeps2  33084  islininds2  33085  isldepslvec2  33086  ldepslinc  33110  zfregs2VD  33641  bnj168  33785  bnj1185  33852  bnj1542  33915  bnj865  33981  bnj916  33991  bnj983  34009  bnj1176  34061  bnj1189  34065  bnj1296  34077  bnj1398  34090  bnj1450  34106  bnj1463  34111  bj-rexcom4a  34446  bj-rexcom4bv  34447  bj-rexcom4b  34448  bj-elsngl  34526  islshpat  34742  lshpsmreu  34834  2dim  35194  islpln5  35259  lplnexatN  35287  islvol5  35303  dalem18  35405  dalem20  35417  lhpexle2  35734  lhpexle3  35736  lhpex2leN  35737  4atex2  35801  4atex2-0bOLDN  35803  cdlemftr3  36291  cdlemg17pq  36398  cdlemg19  36410  cdlemg21  36412  cdlemg33d  36435  dva1dim  36711  dih1dimatlem  37056  dihglb2  37069  dvh2dim  37172  mapdrvallem2  37372  mapdpglem3  37402  hdmapglem7a  37657  elimaint  37764  elintima  37765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-rex 2813
  Copyright terms: Public domain W3C validator