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

Theorem rexbii 2906
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 692 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2904 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1842   E.wrex 2755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-rex 2760
This theorem is referenced by:  2rexbii  2907  rexnal2  2908  rexnal3  2909  ralnex3  2911  rexanaliOLD  2912  r19.29r  2943  r19.29imd  2944  r19.41vv  2961  r19.42v  2962  r19.43  2963  rexcom13  2970  rexrot4  2971  3reeanv  2976  2ralor  2977  cbvrex2v  3043  rexcom4  3079  rexcom4a  3080  rexcom4b  3081  ceqsrex2v  3185  reu7  3244  0el  3756  uni0b  4216  rabasiun  4275  iuncom  4278  iuncom4  4279  iuniin  4282  dfiunv2  4307  iunab  4317  iunn0  4331  iunin2  4335  iundif2  4338  iunun  4355  iunxiun  4357  iunpwss  4364  inuni  4556  reusv2lem5  4599  reuxfrd  4616  iunopab  4726  dffr2  4788  frc  4789  frminex  4803  dfepfr  4808  epfrc  4809  xpiundi  4878  xpiundir  4879  reliin  4944  iunxpf  4972  cnvuni  5010  dmiun  5032  dfima3  5160  dffr3  5189  rniun  5234  xpdifid  5253  dminxp  5265  imaco  5328  coiun  5333  dffr4  5383  tz6.26  5398  sucel  5483  isarep1  5648  rexrn  6011  ralrn  6012  elrnrexdmb  6014  fnasrn  6057  rexima  6132  ralima  6133  abrexco  6137  imaiun  6138  fliftcnv  6192  rexrnmpt2  6399  iunpw  6596  abrexex2g  6761  abrexex2  6765  el2xptp  6827  rdglem1  7118  tz7.49  7147  oarec  7248  omeu  7271  qsid  7414  eroveu  7443  ixp0  7540  fimax2g  7800  marypha2lem2  7930  dfsup2  7936  dfsup2OLD  7937  dfoi  7970  wemapsolem  8009  zfregcl  8054  zfreg  8055  zfreg2  8056  oemapso  8133  zfregs2  8196  infenaleph  8504  isinfcard  8505  kmlem7  8568  kmlem13  8574  fin23lem26  8737  dffin1-5  8800  fin12  8825  numth  8884  ac6n  8897  zorn2lem7  8914  zorng  8916  brdom7disj  8941  brdom6disj  8942  uniwun  9148  axgroth5  9232  axgroth4  9240  grothprim  9242  npomex  9404  genpass  9417  elreal  9538  dfinfmr  10560  infmsup  10561  infmrgelb  10563  infmrlb  10564  uzwo  11190  ublbneg  11211  xrinfmss2  11555  4fvwrd4  11848  fsuppmapnn0fiubex  12142  fsuppmapnn0ub  12145  mptnn0fsuppr  12149  hashge2el2dif  12570  wrdlen1  12632  dfrtrclrec2  13039  rexanuz  13327  rexfiuz  13329  clim0  13478  cbvsum  13666  incexc2  13801  cbvprod  13874  iprodmul  13948  divalglem10  14269  divalgb  14271  pythagtriplem2  14550  pythagtriplem19  14566  pythagtrip  14567  pceu  14579  prmreclem6  14648  4sqlem12  14683  cshwshashlem1  14789  cshwshash  14798  imasaddfnlem  15142  isdrs2  15892  symgmov1  16741  pmtrprfvalrn  16837  pgpfac1lem5  17450  dvdsrval  17614  opprunit  17630  lsmspsn  18050  lsmelval2  18051  islpidl  18214  mat1dimelbas  19265  mat1dimbas  19266  mdetunilem8  19413  pmatcollpw2lem  19570  tgval2  19749  ntreq0  19871  isclo2  19882  neiptopnei  19926  ist0-3  20139  tgcmp  20194  cmpfi  20201  is1stc2  20235  unisngl  20320  xkobval  20379  txtube  20433  txcmplem1  20434  xkococnlem  20452  eltsms  20923  metrest  21319  iscau3  22009  bcth  22060  pmltpc  22154  itg2i1fseq  22454  itg2cn  22462  plyun0  22886  aaliou3lem9  23038  1cubr  23498  dchrvmasumlema  24066  selbergsb  24141  ostth  24205  istrkg2ld  24236  tglowdim1i  24273  tgdim01  24279  legtrid  24361  midex  24497  brbtwn2  24625  colinearalg  24630  ax5seg  24658  axpasch  24661  axlowdimlem6  24667  axeuclidlem  24682  axeuclid  24683  usgra2edg1  24800  nbgraop1  24842  nbgraf1olem1  24858  el2wlkonot  25286  el2spthonot  25287  el2wlkonotot0  25289  4cycl2vnunb  25434  vdn0frgrav2  25440  vdgn0frgrav2  25441  usg2spot2nb  25482  usgreg2spot  25484  numclwwlkun  25496  lpni  25599  isgrpo2  25613  isgrp2d  25651  nmobndseqi  26108  hhcmpl  26531  shne0i  26780  nmcopexi  27359  nmcfnexi  27383  cdj3lem3b  27772  rexcom4f  27789  iunin1f  27853  disjunsn  27886  ofpreima  27950  fpwrelmapffslem  28002  tosglblem  28109  xrnarchi  28180  ordtconlem1  28359  lmdvg  28388  esumfsup  28517  bnj168  29112  bnj1185  29179  bnj1542  29242  bnj865  29308  bnj916  29318  bnj983  29336  bnj1176  29388  bnj1189  29392  bnj1296  29404  bnj1398  29417  bnj1450  29433  bnj1463  29438  cvmliftlem15  29595  cvmlift2lem12  29611  dffr5  29966  dfon2lem9  30010  soseq  30065  nodenselem4  30144  nodenselem5  30145  nofulllem5  30166  brbigcup  30236  elfuns  30253  brimage  30264  brimg  30275  dfrecs2  30288  imagesset  30291  brub  30292  brsegle  30446  gtinf  30547  filnetlem4  30609  bj-rexcom4a  31010  bj-rexcom4bv  31011  bj-rexcom4b  31012  bj-elsngl  31091  iundif1  31409  ismblfin  31427  volsupnfl  31431  itg2addnclem3  31441  fdc  31520  isfldidl  31747  prtlem10  31888  prter2  31904  islshpat  32035  lshpsmreu  32127  2dim  32487  islpln5  32552  lplnexatN  32580  islvol5  32596  dalem18  32698  dalem20  32710  lhpexle2  33027  lhpexle3  33029  lhpex2leN  33030  4atex2  33094  4atex2-0bOLDN  33096  cdlemftr3  33584  cdlemg17pq  33691  cdlemg19  33703  cdlemg21  33705  cdlemg33d  33728  dva1dim  34004  dih1dimatlem  34349  dihglb2  34362  dvh2dim  34465  mapdrvallem2  34665  mapdpglem3  34695  hdmapglem7a  34950  elrfirn  34989  isnacs2  35000  isnacs3  35004  sbc2rex  35082  4rexfrabdioph  35093  eldioph4b  35106  fphpd  35111  fiphp3d  35114  rencldnfilem  35115  rmxdioph  35320  expdiophlem1  35325  islnm2  35386  phisum  35523  elimaint  35627  cnviun  35629  imaiun1  35630  coiun1  35631  elintima  35632  briunov2  35661  prmunb2  36039  zfregs2VD  36671  evth2f  36770  evthf  36782  fprodle  36972  stoweidlem28  37178  fourierdlem63  37320  fourierdlem65  37322  fourierdlem89  37346  fourierdlem90  37347  fourierdlem91  37348  fourierdlem100  37357  2rexsb  37543  2rexrsb  37544  cbvrex2  37546  2reu5a  37550  usgra2pth0  37984  usgvincvad  38033  usgvincvadALT  38036  usg2edgneu  38041  copisnmnd  38126  pgrpgt2nabl  38470  islindeps  38565  lindslinindsimp1  38569  lindslinindsimp2  38575  islindeps2  38595  islininds2  38596  isldepslvec2  38597  ldepslinc  38621
  Copyright terms: Public domain W3C validator