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

Theorem rexbii 2888
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 699 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2886 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    e. wcel 1886   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-rex 2742
This theorem is referenced by:  2rexbii  2889  rexnal2  2890  rexnal3  2891  ralnex3  2893  rexanaliOLD  2894  r19.29r  2925  r19.29imd  2926  r19.41vv  2943  r19.42v  2944  r19.43  2945  rexcom13  2952  rexrot4  2953  3reeanv  2958  2ralor  2959  cbvrex2v  3027  rexcom4  3066  rexcom4a  3067  rexcom4b  3068  ceqsrex2v  3173  reu7  3232  0el  3748  uni0b  4222  rabasiun  4281  iuncom  4284  iuncom4  4285  iuniin  4288  dfiunv2  4313  iunab  4323  iunn0  4337  iunin2  4341  iundif2  4344  iunun  4361  iunxiun  4363  iunpwss  4370  inuni  4564  reusv2lem5  4607  reuxfrd  4624  iunopab  4736  dffr2  4798  frc  4799  frminex  4813  dfepfr  4818  epfrc  4819  xpiundi  4888  xpiundir  4889  reliin  4954  iunxpf  4982  cnvuni  5020  dmiun  5042  dfima3  5170  dffr3  5200  rniun  5245  xpdifid  5264  dminxp  5276  imaco  5339  coiun  5344  dffr4  5395  tz6.26  5410  sucel  5495  isarep1  5660  rexrn  6022  ralrn  6023  elrnrexdmb  6025  fnasrn  6068  rexima  6142  ralima  6143  abrexco  6147  imaiun  6148  fliftcnv  6202  rexrnmpt2  6409  iunpw  6602  abrexex2g  6767  abrexex2  6771  el2xptp  6833  rdglem1  7130  tz7.49  7159  oarec  7260  omeu  7283  qsid  7426  eroveu  7455  ixp0  7552  fimax2g  7814  marypha2lem2  7947  dfsup2  7955  infcllem  8000  dfoi  8023  wemapsolem  8062  zfregcl  8106  zfreg  8107  zfreg2  8108  oemapso  8184  zfregs2  8214  infenaleph  8519  isinfcard  8520  kmlem7  8583  kmlem13  8589  fin23lem26  8752  dffin1-5  8815  fin12  8840  numth  8899  ac6n  8912  zorn2lem7  8929  zorng  8931  brdom7disj  8956  brdom6disj  8957  uniwun  9162  axgroth5  9246  axgroth4  9254  grothprim  9256  npomex  9418  genpass  9431  elreal  9552  dfinfre  10585  dfinfmrOLD  10586  infrenegsup  10588  infmsupOLD  10589  infmrgelbOLD  10592  infmrlbOLD  10594  uzwo  11219  ublbneg  11245  xrinfmss2  11593  4fvwrd4  11906  fsuppmapnn0fiubex  12201  fsuppmapnn0ub  12204  mptnn0fsuppr  12208  hashge2el2dif  12634  wrdlen1  12702  dfrtrclrec2  13113  rexanuz  13401  rexfiuz  13403  clim0  13563  cbvsum  13754  incexc2  13889  cbvprod  13962  fprodle  14043  iprodmul  14049  divalglem10  14376  divalgb  14378  ncoprmlnprm  14670  pythagtriplem2  14760  pythagtriplem19  14776  pythagtrip  14777  pceu  14789  prmreclem6  14858  4sqlem12  14893  cshwshashlem1  15059  cshwshash  15068  imasaddfnlem  15427  isdrs2  16177  symgmov1  17026  pmtrprfvalrn  17122  pgpfac1lem5  17705  dvdsrval  17866  opprunit  17882  lsmspsn  18300  lsmelval2  18301  islpidl  18463  mat1dimelbas  19489  mat1dimbas  19490  mdetunilem8  19637  pmatcollpw2lem  19794  tgval2  19964  ntreq0  20086  isclo2  20097  neiptopnei  20141  ist0-3  20354  tgcmp  20409  cmpfi  20416  is1stc2  20450  unisngl  20535  xkobval  20594  txtube  20648  txcmplem1  20649  xkococnlem  20667  eltsms  21140  metrest  21532  iscau3  22241  bcth  22290  pmltpc  22394  itg2i1fseq  22706  itg2cn  22714  plyun0  23144  aaliou3lem9  23299  1cubr  23761  dchrvmasumlema  24331  selbergsb  24406  ostth  24470  istrkg2ld  24501  tglowdim1i  24538  tgdim01  24544  legtrid  24629  midex  24772  ishpg  24794  brbtwn2  24928  colinearalg  24933  ax5seg  24961  axpasch  24964  axlowdimlem6  24970  axeuclidlem  24985  axeuclid  24986  usgra2edg1  25103  nbgraop1  25146  nbgraf1olem1  25162  el2wlkonot  25590  el2spthonot  25591  el2wlkonotot0  25593  4cycl2vnunb  25738  vdn0frgrav2  25744  vdgn0frgrav2  25745  usg2spot2nb  25786  usgreg2spot  25788  numclwwlkun  25800  lpni  25904  isgrpo2  25918  isgrp2d  25956  nmobndseqi  26413  hhcmpl  26846  shne0i  27094  nmcopexi  27673  nmcfnexi  27697  cdj3lem3b  28086  rexcom4f  28104  iunin1f  28164  disjunsn  28197  ofpreima  28261  fpwrelmapffslem  28310  tosglblem  28423  xrnarchi  28494  ordtconlem1  28723  lmdvg  28752  esumfsup  28884  bnj168  29531  bnj1185  29598  bnj1542  29661  bnj865  29727  bnj916  29737  bnj983  29755  bnj1176  29807  bnj1189  29811  bnj1296  29823  bnj1398  29836  bnj1450  29852  bnj1463  29857  cvmliftlem15  30014  cvmlift2lem12  30030  dffr5  30386  dfon2lem9  30430  soseq  30485  noseponlem  30548  nosepon  30549  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  31472  bj-rexcom4bv  31473  bj-rexcom4b  31474  bj-elsngl  31555  bj-mpt2mptALT  31624  iundif1  31920  poimirlem1  31934  poimirlem30  31963  poimirlem32  31965  poimir  31966  ismblfin  31974  volsupnfl  31978  itg2addnclem3  31988  fdc  32067  isfldidl  32294  prtlem10  32431  prter2  32447  islshpat  32577  lshpsmreu  32669  2dim  33029  islpln5  33094  lplnexatN  33122  islvol5  33138  dalem18  33240  dalem20  33252  lhpexle2  33569  lhpexle3  33571  lhpex2leN  33572  4atex2  33636  4atex2-0bOLDN  33638  cdlemftr3  34126  cdlemg17pq  34233  cdlemg19  34245  cdlemg21  34247  cdlemg33d  34270  dva1dim  34546  dih1dimatlem  34891  dihglb2  34904  dvh2dim  35007  mapdrvallem2  35207  mapdpglem3  35237  hdmapglem7a  35492  elrfirn  35531  isnacs2  35542  isnacs3  35546  sbc2rex  35624  4rexfrabdioph  35635  eldioph4b  35648  fphpd  35653  fiphp3d  35656  rencldnfilem  35657  rmxdioph  35865  expdiophlem1  35870  islnm2  35930  phisum  36070  elimaint  36234  cnviun  36236  imaiun1  36237  coiun1  36238  elintima  36239  briunov2  36268  prmunb2  36653  zfregs2VD  37231  evth2f  37330  evthf  37342  ndisj2  37383  stoweidlem28  37882  fourierdlem63  38027  fourierdlem65  38029  fourierdlem89  38053  fourierdlem90  38054  fourierdlem91  38055  fourierdlem100  38064  ovn0  38382  2rexsb  38585  2rexrsb  38586  cbvrex2  38588  2reu5a  38592  n0snor2el  38990  usgr2edg1  39278  nbgrsym  39420  isuvtxa  39450  usgra2pth0  39656  usgvincvad  39703  usgvincvadALT  39706  usg2edgneu  39711  copisnmnd  39796  pgrpgt2nabl  40138  islindeps  40233  lindslinindsimp1  40237  lindslinindsimp2  40243  islindeps2  40263  islininds2  40264  isldepslvec2  40265  ldepslinc  40289
  Copyright terms: Public domain W3C validator