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

Theorem rexbii 2958
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 2956 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1762   E.wrex 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-rex 2813
This theorem is referenced by:  2rexbii  2959  rexanaliOLD  2960  r19.29r  2991  r19.29imd  2992  r19.41vv  3008  r19.42v  3009  r19.43  3010  rexcom13  3017  rexrot4  3018  3reeanv  3023  2ralor  3024  cbvrex2v  3090  rexcom4  3126  rexcom4a  3127  rexcom4b  3128  ceqsrex2v  3232  reu7  3291  0el  3795  uni0b  4263  rabasiun  4322  iuncom  4325  iuncom4  4326  iuniin  4329  dfiunv2  4354  iunab  4364  iunn0  4378  iunin2  4382  iundif2  4385  iunun  4399  iunxiun  4401  iunpwss  4408  inuni  4602  reusv2lem5  4645  reusv5OLD  4650  reusv7OLD  4652  reuxfrd  4665  iunopab  4776  dffr2  4837  frc  4838  frminex  4852  dfepfr  4857  epfrc  4858  sucel  4944  xpiundi  5046  xpiundir  5047  reliin  5115  iunxpf  5142  cnvuni  5180  dmiun  5202  dfima3  5331  dffr3  5360  rniun  5407  xpdifid  5426  dminxp  5438  imaco  5503  coiun  5508  isarep1  5658  rexrn  6014  ralrn  6015  elrnrexdmb  6017  fnasrn  6058  rexima  6130  ralima  6131  abrexco  6135  imaiun  6136  fliftcnv  6188  rexrnmpt2  6393  iunpw  6585  abrexex2g  6751  abrexex2  6755  el2xptp  6817  rdglem1  7071  tz7.49  7100  oarec  7201  omeu  7224  qsid  7367  eroveu  7396  ixp0  7492  fimax2g  7755  marypha2lem2  7885  dfsup2  7891  dfsup2OLD  7892  dfoi  7925  wemapsolem  7964  zfregcl  8009  zfreg  8010  zfreg2  8011  oemapso  8090  zfregs2  8153  infenaleph  8461  isinfcard  8462  kmlem7  8525  kmlem13  8531  fin23lem26  8694  dffin1-5  8757  fin12  8782  numth  8841  ac6n  8854  zorn2lem7  8871  zorng  8873  brdom7disj  8898  brdom6disj  8899  uniwun  9107  axgroth5  9191  axgroth4  9199  grothprim  9201  npomex  9363  genpass  9376  elreal  9497  dfinfmr  10509  infmsup  10510  infmrgelb  10512  infmrlb  10513  uzwo  11133  uzwoOLD  11134  ublbneg  11155  xrinfmss2  11491  4fvwrd4  11779  fsuppmapnn0fiubex  12054  fsuppmapnn0ub  12057  mptnn0fsuppr  12061  hashge2el2dif  12474  wrdlen1  12531  rexanuz  13127  rexfiuz  13129  clim0  13278  cbvsum  13466  incexc2  13602  divalglem10  13908  divalgb  13910  pythagtriplem2  14189  pythagtriplem19  14205  pythagtrip  14206  pceu  14218  prmreclem6  14287  4sqlem12  14322  cshwshashlem1  14427  cshwshash  14436  imasaddfnlem  14772  isdrs2  15415  symgmov1  16205  symgmov2  16206  pmtrprfvalrn  16302  pgpfac1lem5  16913  dvdsrval  17071  opprunit  17087  lsmspsn  17506  lsmelval2  17507  islpidl  17669  mat1dimelbas  18733  mat1dimbas  18734  mdetunilem8  18881  pmatcollpw2lem  19038  tgval2  19217  ntreq0  19337  isclo2  19348  neiptopnei  19392  ist0-3  19605  tgcmp  19660  cmpfi  19667  is1stc2  19702  xkobval  19815  txtube  19869  txcmplem1  19870  xkococnlem  19888  eltsms  20359  metrest  20755  iscau3  21445  bcth  21496  pmltpc  21590  itg2i1fseq  21890  itg2cn  21898  plyun0  22322  aaliou3lem9  22473  1cubr  22894  dchrvmasumlema  23406  selbergsb  23481  ostth  23545  istrkg2ld  23579  tglowdim1i  23613  tgdim01  23619  legtrid  23698  mideu  23807  brbtwn2  23877  colinearalg  23882  ax5seg  23910  axpasch  23913  axlowdimlem6  23919  axeuclidlem  23934  axeuclid  23935  usgra2edg1  24045  nbgraop1  24087  nbgraf1olem1  24103  el2wlkonot  24531  el2spthonot  24532  el2wlkonotot0  24534  lpni  24707  isgrpo2  24725  isgrp2d  24763  nmobndseqi  25220  hhcmpl  25643  shne0i  25892  nmcopexi  26472  nmcfnexi  26496  cdj3lem3b  26885  rexcom4f  26902  disjunsn  26976  ofpreima  27029  fpwrelmapffslem  27077  tosglblem  27169  xrnarchi  27240  archiabl  27254  ordtconlem1  27392  lmdvg  27421  esumfsup  27566  cvmliftlem15  28233  cvmlift2lem12  28249  dfrtrclrec2  28391  cbvprod  28474  iprodmul  28549  dffr5  28609  dfon2lem9  28650  dffr4  28689  tz6.26  28712  soseq  28761  nodenselem4  28871  nodenselem5  28872  nofulllem5  28893  brbigcup  28975  elfuns  28992  brimage  29003  brimg  29014  tfrqfree  29028  imagesset  29030  brub  29031  brsegle  29185  iundif1  29464  ismblfin  29483  volsupnfl  29487  itg2addnclem3  29496  gtinf  29565  nn0prpw  29569  filnetlem4  29653  fdc  29692  smprngopr  29903  isfldidl  29919  prtlem10  30061  prter2  30077  elrfirn  30082  isnacs2  30093  isnacs3  30097  sbc2rex  30175  4rexfrabdioph  30186  eldioph4b  30200  fphpd  30205  fiphp3d  30208  rencldnfilem  30209  rmxdioph  30415  expdiophlem1  30420  islnm2  30481  phisum  30617  evth2f  30787  evthf  30799  rexnal2  30824  stoweidlem28  31147  fourierdlem63  31289  fourierdlem65  31291  fourierdlem89  31315  fourierdlem90  31316  fourierdlem91  31317  fourierdlem100  31326  2rexsb  31461  2rexrsb  31462  cbvrex2  31464  2reu5a  31468  usgra2pth0  31643  usgvincvad  31670  usgvincvadALT  31673  usg2edgneu  31678  4cycl2vnunb  31735  vdn0frgrav2  31742  vdgn0frgrav2  31743  usg2spot2nb  31784  usgreg2spot  31786  numclwwlkun  31798  pgrpgt2nabel  31899  islindeps  32002  lindslinindsimp1  32006  lindslinindsimp2  32012  islindeps2  32032  islininds2  32033  isldepslvec2  32034  ldepslinc  32066  zfregs2VD  32596  bnj168  32740  bnj1185  32806  bnj1542  32869  bnj865  32935  bnj916  32945  bnj983  32963  bnj1176  33015  bnj1189  33019  bnj1296  33031  bnj1398  33044  bnj1450  33060  bnj1463  33065  bj-rexcom4a  33402  bj-rexcom4bv  33403  bj-rexcom4b  33404  bj-elsngl  33482  islshpat  33689  lshpsmreu  33781  2dim  34141  islpln5  34206  lplnexatN  34234  islvol5  34250  dalem18  34352  dalem20  34364  lhpexle2  34681  lhpexle3  34683  lhpex2leN  34684  4atex2  34748  4atex2-0bOLDN  34750  cdlemftr3  35236  cdlemg17pq  35343  cdlemg19  35355  cdlemg21  35357  cdlemg33d  35380  dva1dim  35656  dih1dimatlem  36001  dihglb2  36014  dvh2dim  36117  mapdrvallem2  36317  mapdpglem3  36347  hdmapglem7a  36602
  Copyright terms: Public domain W3C validator