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

Theorem rexbii 2943
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  |-  ( ph  <->  ps )
Assertion
Ref Expression
rexbii  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )

Proof of Theorem rexbii
StepHypRef Expression
1 rexbii.1 . . 3  |-  ( ph  <->  ps )
21anbi2i 694 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2941 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1802   E.wrex 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-rex 2797
This theorem is referenced by:  2rexbii  2944  rexnal2  2945  rexanaliOLD  2946  r19.29r  2977  r19.29imd  2978  r19.41vv  2995  r19.42v  2996  r19.43  2997  rexcom13  3004  rexrot4  3005  3reeanv  3010  2ralor  3011  cbvrex2v  3077  rexcom4  3113  rexcom4a  3114  rexcom4b  3115  ceqsrex2v  3219  reu7  3278  0el  3784  uni0b  4255  rabasiun  4315  iuncom  4318  iuncom4  4319  iuniin  4322  dfiunv2  4347  iunab  4357  iunn0  4371  iunin2  4375  iundif2  4378  iunun  4392  iunxiun  4394  iunpwss  4401  inuni  4595  reusv2lem5  4638  reusv5OLD  4643  reusv7OLD  4645  reuxfrd  4658  iunopab  4769  dffr2  4830  frc  4831  frminex  4845  dfepfr  4850  epfrc  4851  sucel  4937  xpiundi  5040  xpiundir  5041  reliin  5110  iunxpf  5137  cnvuni  5175  dmiun  5197  dfima3  5326  dffr3  5355  rniun  5402  xpdifid  5421  dminxp  5433  imaco  5498  coiun  5503  isarep1  5653  rexrn  6014  ralrn  6015  elrnrexdmb  6017  fnasrn  6058  rexima  6132  ralima  6133  abrexco  6137  imaiun  6138  fliftcnv  6190  rexrnmpt2  6399  iunpw  6595  abrexex2g  6758  abrexex2  6762  el2xptp  6824  rdglem1  7079  tz7.49  7108  oarec  7209  omeu  7232  qsid  7375  eroveu  7404  ixp0  7500  fimax2g  7764  marypha2lem2  7894  dfsup2  7900  dfsup2OLD  7901  dfoi  7934  wemapsolem  7973  zfregcl  8018  zfreg  8019  zfreg2  8020  oemapso  8099  zfregs2  8162  infenaleph  8470  isinfcard  8471  kmlem7  8534  kmlem13  8540  fin23lem26  8703  dffin1-5  8766  fin12  8791  numth  8850  ac6n  8863  zorn2lem7  8880  zorng  8882  brdom7disj  8907  brdom6disj  8908  uniwun  9116  axgroth5  9200  axgroth4  9208  grothprim  9210  npomex  9372  genpass  9385  elreal  9506  dfinfmr  10521  infmsup  10522  infmrgelb  10524  infmrlb  10525  uzwo  11148  uzwoOLD  11149  ublbneg  11170  xrinfmss2  11506  4fvwrd4  11796  fsuppmapnn0fiubex  12072  fsuppmapnn0ub  12075  mptnn0fsuppr  12079  hashge2el2dif  12495  wrdlen1  12553  rexanuz  13152  rexfiuz  13154  clim0  13303  cbvsum  13491  incexc2  13624  divalglem10  13932  divalgb  13934  pythagtriplem2  14213  pythagtriplem19  14229  pythagtrip  14230  pceu  14242  prmreclem6  14311  4sqlem12  14346  cshwshashlem1  14452  cshwshash  14461  imasaddfnlem  14797  isdrs2  15437  symgmov1  16286  pmtrprfvalrn  16382  pgpfac1lem5  16998  dvdsrval  17162  opprunit  17178  lsmspsn  17598  lsmelval2  17599  islpidl  17762  mat1dimelbas  18840  mat1dimbas  18841  mdetunilem8  18988  pmatcollpw2lem  19145  tgval2  19324  ntreq0  19444  isclo2  19455  neiptopnei  19499  ist0-3  19712  tgcmp  19767  cmpfi  19774  is1stc2  19809  unisngl  19894  xkobval  19953  txtube  20007  txcmplem1  20008  xkococnlem  20026  eltsms  20497  metrest  20893  iscau3  21583  bcth  21634  pmltpc  21728  itg2i1fseq  22028  itg2cn  22036  plyun0  22460  aaliou3lem9  22611  1cubr  23038  dchrvmasumlema  23550  selbergsb  23625  ostth  23689  istrkg2ld  23723  tglowdim1i  23757  tgdim01  23763  legtrid  23843  midex  23976  brbtwn2  24073  colinearalg  24078  ax5seg  24106  axpasch  24109  axlowdimlem6  24115  axeuclidlem  24130  axeuclid  24131  usgra2edg1  24248  nbgraop1  24290  nbgraf1olem1  24306  el2wlkonot  24734  el2spthonot  24735  el2wlkonotot0  24737  4cycl2vnunb  24882  vdn0frgrav2  24888  vdgn0frgrav2  24889  usg2spot2nb  24930  usgreg2spot  24932  numclwwlkun  24944  lpni  25046  isgrpo2  25064  isgrp2d  25102  nmobndseqi  25559  hhcmpl  25982  shne0i  26231  nmcopexi  26811  nmcfnexi  26835  cdj3lem3b  27224  rexcom4f  27241  disjunsn  27318  ofpreima  27372  fpwrelmapffslem  27420  tosglblem  27523  xrnarchi  27594  ordtconlem1  27772  lmdvg  27801  esumfsup  27942  cvmliftlem15  28609  cvmlift2lem12  28625  dfrtrclrec2  28932  cbvprod  29015  iprodmul  29090  dffr5  29150  dfon2lem9  29191  dffr4  29230  tz6.26  29253  soseq  29302  nodenselem4  29412  nodenselem5  29413  nofulllem5  29434  brbigcup  29516  elfuns  29533  brimage  29544  brimg  29555  tfrqfree  29569  imagesset  29571  brub  29572  brsegle  29726  iundif1  30005  ismblfin  30023  volsupnfl  30027  itg2addnclem3  30036  gtinf  30105  filnetlem4  30167  fdc  30206  isfldidl  30433  prtlem10  30574  prter2  30590  elrfirn  30595  isnacs2  30606  isnacs3  30610  sbc2rex  30688  4rexfrabdioph  30699  eldioph4b  30713  fphpd  30718  fiphp3d  30721  rencldnfilem  30722  rmxdioph  30926  expdiophlem1  30931  islnm2  30992  phisum  31128  prmunb2  31160  evth2f  31337  evthf  31349  stoweidlem28  31695  fourierdlem63  31837  fourierdlem65  31839  fourierdlem89  31863  fourierdlem90  31864  fourierdlem91  31865  fourierdlem100  31874  2rexsb  32009  2rexrsb  32010  cbvrex2  32012  2reu5a  32016  usgra2pth0  32189  usgvincvad  32238  usgvincvadALT  32241  usg2edgneu  32246  copisnmnd  32330  pgrpgt2nabl  32667  islindeps  32764  lindslinindsimp1  32768  lindslinindsimp2  32774  islindeps2  32794  islininds2  32795  isldepslvec2  32796  ldepslinc  32820  zfregs2VD  33349  bnj168  33493  bnj1185  33559  bnj1542  33622  bnj865  33688  bnj916  33698  bnj983  33716  bnj1176  33768  bnj1189  33772  bnj1296  33784  bnj1398  33797  bnj1450  33813  bnj1463  33818  bj-rexcom4a  34158  bj-rexcom4bv  34159  bj-rexcom4b  34160  bj-elsngl  34238  islshpat  34444  lshpsmreu  34536  2dim  34896  islpln5  34961  lplnexatN  34989  islvol5  35005  dalem18  35107  dalem20  35119  lhpexle2  35436  lhpexle3  35438  lhpex2leN  35439  4atex2  35503  4atex2-0bOLDN  35505  cdlemftr3  35993  cdlemg17pq  36100  cdlemg19  36112  cdlemg21  36114  cdlemg33d  36137  dva1dim  36413  dih1dimatlem  36758  dihglb2  36771  dvh2dim  36874  mapdrvallem2  37074  mapdpglem3  37104  hdmapglem7a  37359
  Copyright terms: Public domain W3C validator