MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexbii Structured version   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  |-  ( 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 2957 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1819   E.wrex 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-rex 2813
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  3811  uni0b  4276  rabasiun  4336  iuncom  4339  iuncom4  4340  iuniin  4343  dfiunv2  4368  iunab  4378  iunn0  4392  iunin2  4396  iundif2  4399  iunun  4416  iunxiun  4418  iunpwss  4425  inuni  4618  reusv2lem5  4661  reusv5OLD  4666  reusv7OLD  4668  reuxfrd  4681  iunopab  4792  dffr2  4853  frc  4854  frminex  4868  dfepfr  4873  epfrc  4874  sucel  4960  xpiundi  5063  xpiundir  5064  reliin  5133  iunxpf  5161  cnvuni  5199  dmiun  5221  dfima3  5350  dffr3  5379  rniun  5423  xpdifid  5442  dminxp  5454  imaco  5518  coiun  5523  isarep1  5673  rexrn  6034  ralrn  6035  elrnrexdmb  6037  fnasrn  6078  rexima  6152  ralima  6153  abrexco  6157  imaiun  6158  fliftcnv  6210  rexrnmpt2  6417  iunpw  6613  abrexex2g  6776  abrexex2  6780  el2xptp  6842  rdglem1  7099  tz7.49  7128  oarec  7229  omeu  7252  qsid  7395  eroveu  7424  ixp0  7521  fimax2g  7784  marypha2lem2  7914  dfsup2  7920  dfsup2OLD  7921  dfoi  7954  wemapsolem  7993  zfregcl  8038  zfreg  8039  zfreg2  8040  oemapso  8118  zfregs2  8181  infenaleph  8489  isinfcard  8490  kmlem7  8553  kmlem13  8559  fin23lem26  8722  dffin1-5  8785  fin12  8810  numth  8869  ac6n  8882  zorn2lem7  8899  zorng  8901  brdom7disj  8926  brdom6disj  8927  uniwun  9135  axgroth5  9219  axgroth4  9227  grothprim  9229  npomex  9391  genpass  9404  elreal  9525  dfinfmr  10540  infmsup  10541  infmrgelb  10543  infmrlb  10544  uzwo  11169  uzwoOLD  11170  ublbneg  11191  xrinfmss2  11527  4fvwrd4  11819  fsuppmapnn0fiubex  12101  fsuppmapnn0ub  12104  mptnn0fsuppr  12108  hashge2el2dif  12525  wrdlen1  12587  rexanuz  13190  rexfiuz  13192  clim0  13341  cbvsum  13529  incexc2  13662  cbvprod  13734  iprodmul  13808  divalglem10  14072  divalgb  14074  pythagtriplem2  14353  pythagtriplem19  14369  pythagtrip  14370  pceu  14382  prmreclem6  14451  4sqlem12  14486  cshwshashlem1  14592  cshwshash  14601  imasaddfnlem  14945  isdrs2  15695  symgmov1  16544  pmtrprfvalrn  16640  pgpfac1lem5  17257  dvdsrval  17421  opprunit  17437  lsmspsn  17857  lsmelval2  17858  islpidl  18021  mat1dimelbas  19100  mat1dimbas  19101  mdetunilem8  19248  pmatcollpw2lem  19405  tgval2  19584  ntreq0  19705  isclo2  19716  neiptopnei  19760  ist0-3  19973  tgcmp  20028  cmpfi  20035  is1stc2  20069  unisngl  20154  xkobval  20213  txtube  20267  txcmplem1  20268  xkococnlem  20286  eltsms  20757  metrest  21153  iscau3  21843  bcth  21894  pmltpc  21988  itg2i1fseq  22288  itg2cn  22296  plyun0  22720  aaliou3lem9  22872  1cubr  23299  dchrvmasumlema  23811  selbergsb  23886  ostth  23950  istrkg2ld  23984  tglowdim1i  24018  tgdim01  24024  legtrid  24104  midex  24237  brbtwn2  24335  colinearalg  24340  ax5seg  24368  axpasch  24371  axlowdimlem6  24377  axeuclidlem  24392  axeuclid  24393  usgra2edg1  24510  nbgraop1  24552  nbgraf1olem1  24568  el2wlkonot  24996  el2spthonot  24997  el2wlkonotot0  24999  4cycl2vnunb  25144  vdn0frgrav2  25150  vdgn0frgrav2  25151  usg2spot2nb  25192  usgreg2spot  25194  numclwwlkun  25206  lpni  25308  isgrpo2  25326  isgrp2d  25364  nmobndseqi  25821  hhcmpl  26244  shne0i  26493  nmcopexi  27073  nmcfnexi  27097  cdj3lem3b  27486  rexcom4f  27503  iunin1f  27562  disjunsn  27593  ofpreima  27661  fpwrelmapffslem  27712  tosglblem  27817  xrnarchi  27888  ordtconlem1  28067  lmdvg  28096  esumfsup  28242  cvmliftlem15  28940  cvmlift2lem12  28956  dfrtrclrec2  29284  dffr5  29400  dfon2lem9  29440  dffr4  29479  tz6.26  29502  soseq  29551  nodenselem4  29661  nodenselem5  29662  nofulllem5  29683  brbigcup  29753  elfuns  29770  brimage  29781  brimg  29792  tfrqfree  29806  imagesset  29808  brub  29809  brsegle  29963  iundif1  30242  ismblfin  30260  volsupnfl  30264  itg2addnclem3  30273  gtinf  30342  filnetlem4  30404  fdc  30443  isfldidl  30670  prtlem10  30811  prter2  30827  elrfirn  30832  isnacs2  30843  isnacs3  30847  sbc2rex  30925  4rexfrabdioph  30936  eldioph4b  30949  fphpd  30954  fiphp3d  30957  rencldnfilem  30958  rmxdioph  31162  expdiophlem1  31167  islnm2  31228  phisum  31363  prmunb2  31395  evth2f  31593  evthf  31605  fprodle  31807  stoweidlem28  32013  fourierdlem63  32155  fourierdlem65  32157  fourierdlem89  32181  fourierdlem90  32182  fourierdlem91  32183  fourierdlem100  32192  2rexsb  32378  2rexrsb  32379  cbvrex2  32381  2reu5a  32385  usgra2pth0  32617  usgvincvad  32666  usgvincvadALT  32669  usg2edgneu  32674  copisnmnd  32759  pgrpgt2nabl  33103  islindeps  33198  lindslinindsimp1  33202  lindslinindsimp2  33208  islindeps2  33228  islininds2  33229  isldepslvec2  33230  ldepslinc  33254  zfregs2VD  33784  bnj168  33928  bnj1185  33995  bnj1542  34058  bnj865  34124  bnj916  34134  bnj983  34152  bnj1176  34204  bnj1189  34208  bnj1296  34220  bnj1398  34233  bnj1450  34249  bnj1463  34254  bj-rexcom4a  34589  bj-rexcom4bv  34590  bj-rexcom4b  34591  bj-elsngl  34669  islshpat  34885  lshpsmreu  34977  2dim  35337  islpln5  35402  lplnexatN  35430  islvol5  35446  dalem18  35548  dalem20  35560  lhpexle2  35877  lhpexle3  35879  lhpex2leN  35880  4atex2  35944  4atex2-0bOLDN  35946  cdlemftr3  36434  cdlemg17pq  36541  cdlemg19  36553  cdlemg21  36555  cdlemg33d  36578  dva1dim  36854  dih1dimatlem  37199  dihglb2  37212  dvh2dim  37315  mapdrvallem2  37515  mapdpglem3  37545  hdmapglem7a  37800  elimaint  37924  elintima  37925
  Copyright terms: Public domain W3C validator