Theorem rexbii 3041

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

Step	Hyp	Ref	Expression
1		rexbii.1	. . 3 |- ( ph <-> ps )
2	1	anbi2i 730	. 2 |- ( ( x e. A /\ ph ) <-> ( x e. A /\ ps ) )
3	2	rexbii2 3039	1 |- ( E. x e. A ph <-> E. x e. A ps )

Syntax hints:   <-> wb 196   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-rex 2918

This theorem is referenced by:  2rexbii  3042  rexnal2  3043  ralnex3  3046  r19.29r  3073  r19.29imd  3074  r19.41vv  3091  r19.42v  3092  r19.43  3093  rexcom13  3101  rexrot4  3103  3reeanv  3108  2ralor  3109  cbvrex2v  3180  rexcom4  3225  rexcom4a  3226  rexcom4b  3227  ceqsrex2v  3338  reu7  3401  0el  3939  n0snor2el  4364  uni0b  4463  iuncom  4527  iuncom4  4528  iuniin  4531  dfiunv2  4556  iunab  4566  iunn0  4580  iunin2  4584  iundif2  4587  iunun  4604  iunxiun  4608  iunpwss  4618  inuni  4826  reusv2lem5  4873  reuxfrd  4893  iunopab  5012  dffr2  5079  frc  5080  frminex  5094  dfepfr  5099  epfrc  5100  xpiundi  5173  xpiundir  5174  reliin  5240  iunxpf  5270  cnvuni  5309  dmiun  5333  dfima3  5469  dffr3  5498  rniun  5543  xpdifid  5562  dminxp  5574  imaco  5640  coiun  5645  dffr4  5696  tz6.26  5711  sucel  5798  isarep1  5977  rexrn  6361  ralrn  6362  elrnrexdmb  6364  fnasrn  6411  rexima  6497  ralima  6498  abrexco  6502  imaiun  6503  fliftcnv  6561  rexrnmpt2  6776  iunpw  6978  abrexex2g  7144  abrexex2OLD  7150  el2xptp  7211  rdglem1  7511  tz7.49  7540  oarec  7642  omeu  7665  qsid  7813  eroveu  7842  ixp0  7941  fimax2g  8206  marypha2lem2  8342  dfsup2  8350  infcllem  8393  dfoi  8416  wemapsolem  8455  zfregcl  8499  zfreg  8500  zfregclOLD  8501  zfregOLD  8502  zfreg2OLD  8503  zfregfr  8509  oemapso  8579  zfregs2  8609  infenaleph  8914  isinfcard  8915  kmlem7  8978  kmlem13  8984  fin23lem26  9147  dffin1-5  9210  fin12  9235  numth  9294  ac6n  9307  zorn2lem7  9324  zorng  9326  brdom7disj  9353  brdom6disj  9354  uniwun  9562  axgroth5  9646  axgroth4  9654  grothprim  9656  npomex  9818  genpass  9831  elreal  9952  dfinfre  11004  infrenegsup  11006  uzwo  11751  ublbneg  11773  xrinfmss2  12141  4fvwrd4  12459  fsuppmapnn0fiubex  12792  fsuppmapnn0ub  12795  mptnn0fsuppr  12799  hashge2el2dif  13262  wrdlen1  13343  dfrtrclrec2  13797  rexanuz  14085  rexfiuz  14087  clim0  14237  cbvsum  14425  incexc2  14570  cbvprod  14645  fprodle  14727  iprodmul  14734  divalglem10  15125  divalgb  15127  ncoprmlnprm  15436  phisum  15495  pythagtriplem2  15522  pythagtriplem19  15538  pythagtrip  15539  pceu  15551  prmreclem6  15625  4sqlem12  15660  cshwshashlem1  15802  cshwshash  15811  imasaddfnlem  16188  isdrs2  16939  symgmov1  17812  pmtrprfvalrn  17908  pgpfac1lem5  18478  dvdsrval  18645  opprunit  18661  lsmspsn  19084  lsmelval2  19085  islpidl  19246  mat1dimelbas  20277  mat1dimbas  20278  mdetunilem8  20425  pmatcollpw2lem  20582  tgval2  20760  ntreq0  20881  isclo2  20892  neiptopnei  20936  ist0-3  21149  tgcmp  21204  cmpfi  21211  is1stc2  21245  unisngl  21330  xkobval  21389  txtube  21443  txcmplem1  21444  xkococnlem  21462  eltsms  21936  metrest  22329  iscau3  23076  bcth  23126  pmltpc  23219  itg2i1fseq  23522  itg2cn  23530  plyun0  23953  aaliou3lem9  24105  1cubr  24569  dchrvmasumlema  25189  selbergsb  25264  ostth  25328  istrkg2ld  25359  tglowdim1i  25396  tgdim01  25402  legtrid  25486  midex  25629  ishpg  25651  brbtwn2  25785  colinearalg  25790  ax5seg  25818  axpasch  25821  axlowdimlem6  25827  axeuclidlem  25842  axeuclid  25843  umgr2edg1  26103  umgr2edgneu  26106  nbgrsym  26265  isuvtxa  26295  usgr2pth0  26661  wlkiswwlksupgr2  26763  clwwlksnun  26974  4cycl2vnunb  27154  fusgreg2wsp  27200  lpni  27332  nmobndseqi  27634  hhcmpl  28057  shne0i  28307  nmcopexi  28886  nmcfnexi  28910  cdj3lem3b  29299  rexcom4f  29317  iunin1f  29374  ofpreima  29465  fpwrelmapffslem  29507  tosglblem  29669  xrnarchi  29738  ordtconnlem1  29970  lmdvg  29999  esumfsup  30132  reprsuc  30693  reprdifc  30705  bnj168  30798  bnj1185  30864  bnj1542  30927  bnj865  30993  bnj916  31003  bnj983  31021  bnj1176  31073  bnj1189  31077  bnj1296  31089  bnj1398  31102  bnj1450  31118  bnj1463  31123  cvmliftlem15  31280  cvmlift2lem12  31296  dffr5  31643  imaindm  31682  dfon2lem9  31696  soseq  31751  noseponlem  31817  nosepon  31818  nolt02o  31845  brbigcup  32005  elfuns  32022  brimage  32033  brimg  32044  dfrecs2  32057  imagesset  32060  brub  32061  brsegle  32215  gtinfOLD  32314  filnetlem4  32376  bj-rexcom4a  32870  bj-rexcom4bv  32871  bj-rexcom4b  32872  bj-elsngl  32956  bj-rest10  33041  bj-restreg  33052  bj-mpt2mptALT  33072  iundif1  33383  matunitlindflem1  33405  poimirlem1  33410  poimirlem30  33439  poimirlem32  33441  poimir  33442  ismblfin  33450  volsupnfl  33454  itg2addnclem3  33463  fdc  33541  isfldidl  33867  eldmqsres2  34052  n0elqs  34098  prtlem10  34150  prter2  34166  islshpat  34304  lshpsmreu  34396  2dim  34756  islpln5  34821  lplnexatN  34849  islvol5  34865  dalem18  34967  dalem20  34979  lhpexle2  35296  lhpexle3  35298  lhpex2leN  35299  4atex2  35363  4atex2-0bOLDN  35365  cdlemftr3  35853  cdlemg17pq  35960  cdlemg19  35972  cdlemg21  35974  cdlemg33d  35997  dva1dim  36273  dih1dimatlem  36618  dihglb2  36631  dvh2dim  36734  mapdrvallem2  36934  mapdpglem3  36964  hdmapglem7a  37219  elrfirn  37258  isnacs2  37269  isnacs3  37273  sbc2rex  37351  4rexfrabdioph  37362  eldioph4b  37375  fphpd  37380  fiphp3d  37383  rencldnfilem  37384  rmxdioph  37583  expdiophlem1  37588  islnm2  37648  elimaint  37940  cnviun  37942  imaiun1  37943  coiun1  37944  elintima  37945  briunov2  37974  clsk3nimkb  38338  prmunb2  38510  zfregs2VD  39076  evth2f  39174  evthf  39186  ndisj2  39218  fnlimabslt  39911  climbddf  39919  limsupub  39936  limsuppnflem  39942  limsupubuz  39945  limsupre2lem  39956  limsupreuz  39969  limsupvaluz2  39970  cnrefiisplem  40055  cnrefiisp  40056  stoweidlem28  40245  fourierdlem63  40386  fourierdlem65  40388  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem100  40423  sge0pnfmpt  40662  ovn0  40780  smfaddlem1  40971  smflimlem4  40982  2rexsb  41170  2rexrsb  41171  cbvrex2  41173  2reu5a  41177  copisnmnd  41809  pgrpgt2nabl  42147  islindeps  42242  lindslinindsimp1  42246  lindslinindsimp2  42252  islindeps2  42272  islininds2  42273  isldepslvec2  42274  ldepslinc  42298