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

Theorem rexbii 2927
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 698 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2925 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    e. wcel 1868   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-rex 2781
This theorem is referenced by:  2rexbii  2928  rexnal2  2929  rexnal3  2930  ralnex3  2932  rexanaliOLD  2933  r19.29r  2964  r19.29imd  2965  r19.41vv  2982  r19.42v  2983  r19.43  2984  rexcom13  2991  rexrot4  2992  3reeanv  2997  2ralor  2998  cbvrex2v  3064  rexcom4  3101  rexcom4a  3102  rexcom4b  3103  ceqsrex2v  3207  reu7  3266  0el  3779  uni0b  4241  rabasiun  4300  iuncom  4303  iuncom4  4304  iuniin  4307  dfiunv2  4332  iunab  4342  iunn0  4356  iunin2  4360  iundif2  4363  iunun  4380  iunxiun  4382  iunpwss  4389  inuni  4583  reusv2lem5  4626  reuxfrd  4643  iunopab  4753  dffr2  4815  frc  4816  frminex  4830  dfepfr  4835  epfrc  4836  xpiundi  4905  xpiundir  4906  reliin  4971  iunxpf  4999  cnvuni  5037  dmiun  5059  dfima3  5187  dffr3  5217  rniun  5262  xpdifid  5281  dminxp  5293  imaco  5356  coiun  5361  dffr4  5412  tz6.26  5427  sucel  5512  isarep1  5677  rexrn  6036  ralrn  6037  elrnrexdmb  6039  fnasrn  6082  rexima  6156  ralima  6157  abrexco  6161  imaiun  6162  fliftcnv  6216  rexrnmpt2  6423  iunpw  6616  abrexex2g  6781  abrexex2  6785  el2xptp  6847  rdglem1  7138  tz7.49  7167  oarec  7268  omeu  7291  qsid  7434  eroveu  7463  ixp0  7560  fimax2g  7820  marypha2lem2  7953  dfsup2  7961  infcllem  8006  dfoi  8029  wemapsolem  8068  zfregcl  8112  zfreg  8113  zfreg2  8114  oemapso  8189  zfregs2  8219  infenaleph  8523  isinfcard  8524  kmlem7  8587  kmlem13  8593  fin23lem26  8756  dffin1-5  8819  fin12  8844  numth  8903  ac6n  8916  zorn2lem7  8933  zorng  8935  brdom7disj  8960  brdom6disj  8961  uniwun  9166  axgroth5  9250  axgroth4  9258  grothprim  9260  npomex  9422  genpass  9435  elreal  9556  dfinfre  10589  dfinfmrOLD  10590  infrenegsup  10592  infmsupOLD  10593  infmrgelbOLD  10596  infmrlbOLD  10598  uzwo  11223  ublbneg  11249  xrinfmss2  11597  4fvwrd4  11910  fsuppmapnn0fiubex  12204  fsuppmapnn0ub  12207  mptnn0fsuppr  12211  hashge2el2dif  12634  wrdlen1  12698  dfrtrclrec2  13109  rexanuz  13397  rexfiuz  13399  clim0  13558  cbvsum  13749  incexc2  13884  cbvprod  13957  fprodle  14038  iprodmul  14044  divalglem10  14371  divalgb  14373  ncoprmlnprm  14665  pythagtriplem2  14755  pythagtriplem19  14771  pythagtrip  14772  pceu  14784  prmreclem6  14853  4sqlem12  14888  cshwshashlem1  15054  cshwshash  15063  imasaddfnlem  15422  isdrs2  16172  symgmov1  17021  pmtrprfvalrn  17117  pgpfac1lem5  17700  dvdsrval  17861  opprunit  17877  lsmspsn  18295  lsmelval2  18296  islpidl  18458  mat1dimelbas  19483  mat1dimbas  19484  mdetunilem8  19631  pmatcollpw2lem  19788  tgval2  19958  ntreq0  20080  isclo2  20091  neiptopnei  20135  ist0-3  20348  tgcmp  20403  cmpfi  20410  is1stc2  20444  unisngl  20529  xkobval  20588  txtube  20642  txcmplem1  20643  xkococnlem  20661  eltsms  21134  metrest  21526  iscau3  22235  bcth  22284  pmltpc  22388  itg2i1fseq  22700  itg2cn  22708  plyun0  23138  aaliou3lem9  23293  1cubr  23755  dchrvmasumlema  24325  selbergsb  24400  ostth  24464  istrkg2ld  24495  tglowdim1i  24532  tgdim01  24538  legtrid  24623  midex  24766  ishpg  24788  brbtwn2  24922  colinearalg  24927  ax5seg  24955  axpasch  24958  axlowdimlem6  24964  axeuclidlem  24979  axeuclid  24980  usgra2edg1  25097  nbgraop1  25139  nbgraf1olem1  25155  el2wlkonot  25583  el2spthonot  25584  el2wlkonotot0  25586  4cycl2vnunb  25731  vdn0frgrav2  25737  vdgn0frgrav2  25738  usg2spot2nb  25779  usgreg2spot  25781  numclwwlkun  25793  lpni  25897  isgrpo2  25911  isgrp2d  25949  nmobndseqi  26406  hhcmpl  26839  shne0i  27087  nmcopexi  27666  nmcfnexi  27690  cdj3lem3b  28079  rexcom4f  28097  iunin1f  28161  disjunsn  28194  ofpreima  28258  fpwrelmapffslem  28311  tosglblem  28425  xrnarchi  28496  ordtconlem1  28726  lmdvg  28755  esumfsup  28887  bnj168  29534  bnj1185  29601  bnj1542  29664  bnj865  29730  bnj916  29740  bnj983  29758  bnj1176  29810  bnj1189  29814  bnj1296  29826  bnj1398  29839  bnj1450  29855  bnj1463  29860  cvmliftlem15  30017  cvmlift2lem12  30033  dffr5  30388  dfon2lem9  30432  soseq  30487  nodenselem4  30566  nodenselem5  30567  nofulllem5  30588  brbigcup  30658  elfuns  30675  brimage  30686  brimg  30697  dfrecs2  30710  imagesset  30713  brub  30714  brsegle  30868  gtinf  30968  filnetlem4  31030  bj-rexcom4a  31437  bj-rexcom4bv  31438  bj-rexcom4b  31439  bj-elsngl  31518  iundif1  31841  poimirlem1  31855  poimirlem30  31884  poimirlem32  31886  poimir  31887  ismblfin  31895  volsupnfl  31899  itg2addnclem3  31909  fdc  31988  isfldidl  32215  prtlem10  32355  prter2  32371  islshpat  32502  lshpsmreu  32594  2dim  32954  islpln5  33019  lplnexatN  33047  islvol5  33063  dalem18  33165  dalem20  33177  lhpexle2  33494  lhpexle3  33496  lhpex2leN  33497  4atex2  33561  4atex2-0bOLDN  33563  cdlemftr3  34051  cdlemg17pq  34158  cdlemg19  34170  cdlemg21  34172  cdlemg33d  34195  dva1dim  34471  dih1dimatlem  34816  dihglb2  34829  dvh2dim  34932  mapdrvallem2  35132  mapdpglem3  35162  hdmapglem7a  35417  elrfirn  35456  isnacs2  35467  isnacs3  35471  sbc2rex  35549  4rexfrabdioph  35560  eldioph4b  35573  fphpd  35578  fiphp3d  35581  rencldnfilem  35582  rmxdioph  35791  expdiophlem1  35796  islnm2  35856  phisum  35996  elimaint  36100  cnviun  36102  imaiun1  36103  coiun1  36104  elintima  36105  briunov2  36134  prmunb2  36517  zfregs2VD  37098  evth2f  37197  evthf  37209  ndisj2  37251  stoweidlem28  37708  fourierdlem63  37853  fourierdlem65  37855  fourierdlem89  37879  fourierdlem90  37880  fourierdlem91  37881  fourierdlem100  37890  ovn0  38163  2rexsb  38304  2rexrsb  38305  cbvrex2  38307  2reu5a  38311  n0snor2el  38701  usgr2edg1  38915  usgra2pth0  38941  usgvincvad  38988  usgvincvadALT  38991  usg2edgneu  38996  copisnmnd  39081  pgrpgt2nabl  39425  islindeps  39520  lindslinindsimp1  39524  lindslinindsimp2  39530  islindeps2  39550  islininds2  39551  isldepslvec2  39552  ldepslinc  39576
  Copyright terms: Public domain W3C validator