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

Theorem rexbii 2881
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 708 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2879 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    e. wcel 1904   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-rex 2762
This theorem is referenced by:  2rexbii  2882  rexnal2  2883  rexnal3  2884  ralnex3  2886  r19.29r  2913  r19.29imd  2914  r19.41vv  2930  r19.42v  2931  r19.43  2932  rexcom13  2939  rexrot4  2940  3reeanv  2945  2ralor  2946  cbvrex2v  3014  rexcom4  3053  rexcom4a  3054  rexcom4b  3055  ceqsrex2v  3162  reu7  3221  0el  3740  uni0b  4215  rabasiun  4273  iuncom  4276  iuncom4  4277  iuniin  4280  dfiunv2  4305  iunab  4315  iunn0  4329  iunin2  4333  iundif2  4336  iunun  4353  iunxiun  4357  iunpwss  4364  inuni  4563  reusv2lem5  4606  reuxfrd  4625  iunopab  4737  dffr2  4804  frc  4805  frminex  4819  dfepfr  4824  epfrc  4825  xpiundi  4894  xpiundir  4895  reliin  4960  iunxpf  4988  cnvuni  5026  dmiun  5049  dfima3  5177  dffr3  5207  rniun  5252  xpdifid  5271  dminxp  5283  imaco  5347  coiun  5352  dffr4  5403  tz6.26  5418  sucel  5503  isarep1  5672  rexrn  6039  ralrn  6040  elrnrexdmb  6042  fnasrn  6086  rexima  6162  ralima  6163  abrexco  6167  imaiun  6168  fliftcnv  6222  rexrnmpt2  6431  iunpw  6624  abrexex2g  6789  abrexex2  6793  el2xptp  6855  rdglem1  7151  tz7.49  7180  oarec  7281  omeu  7304  qsid  7447  eroveu  7476  ixp0  7573  fimax2g  7835  marypha2lem2  7968  dfsup2  7976  infcllem  8021  dfoi  8044  wemapsolem  8083  zfregcl  8127  zfreg  8128  zfreg2  8129  oemapso  8205  zfregs2  8235  infenaleph  8540  isinfcard  8541  kmlem7  8604  kmlem13  8610  fin23lem26  8773  dffin1-5  8836  fin12  8861  numth  8920  ac6n  8933  zorn2lem7  8950  zorng  8952  brdom7disj  8977  brdom6disj  8978  uniwun  9183  axgroth5  9267  axgroth4  9275  grothprim  9277  npomex  9439  genpass  9452  elreal  9573  dfinfre  10610  dfinfmrOLD  10611  infrenegsup  10613  infmsupOLD  10614  infmrgelbOLD  10617  infmrlbOLD  10619  uzwo  11245  ublbneg  11271  xrinfmss2  11621  4fvwrd4  11936  fsuppmapnn0fiubex  12242  fsuppmapnn0ub  12245  mptnn0fsuppr  12249  hashge2el2dif  12678  wrdlen1  12756  dfrtrclrec2  13197  rexanuz  13485  rexfiuz  13487  clim0  13647  cbvsum  13838  incexc2  13973  cbvprod  14046  fprodle  14127  iprodmul  14133  divalglem10  14462  divalgb  14464  ncoprmlnprm  14756  pythagtriplem2  14846  pythagtriplem19  14862  pythagtrip  14863  pceu  14875  prmreclem6  14944  4sqlem12  14979  cshwshashlem1  15144  cshwshash  15153  imasaddfnlem  15512  isdrs2  16262  symgmov1  17111  pmtrprfvalrn  17207  pgpfac1lem5  17790  dvdsrval  17951  opprunit  17967  lsmspsn  18385  lsmelval2  18386  islpidl  18547  mat1dimelbas  19573  mat1dimbas  19574  mdetunilem8  19721  pmatcollpw2lem  19878  tgval2  20048  ntreq0  20170  isclo2  20181  neiptopnei  20225  ist0-3  20438  tgcmp  20493  cmpfi  20500  is1stc2  20534  unisngl  20619  xkobval  20678  txtube  20732  txcmplem1  20733  xkococnlem  20751  eltsms  21225  metrest  21617  iscau3  22326  bcth  22375  pmltpc  22479  itg2i1fseq  22792  itg2cn  22800  plyun0  23230  aaliou3lem9  23385  1cubr  23847  dchrvmasumlema  24417  selbergsb  24492  ostth  24556  istrkg2ld  24587  tglowdim1i  24624  tgdim01  24630  legtrid  24715  midex  24858  ishpg  24880  brbtwn2  25014  colinearalg  25019  ax5seg  25047  axpasch  25050  axlowdimlem6  25056  axeuclidlem  25071  axeuclid  25072  usgra2edg1  25189  nbgraop1  25232  nbgraf1olem1  25248  el2wlkonot  25676  el2spthonot  25677  el2wlkonotot0  25679  4cycl2vnunb  25824  vdn0frgrav2  25830  vdgn0frgrav2  25831  usg2spot2nb  25872  usgreg2spot  25874  numclwwlkun  25886  lpni  25990  isgrpo2  26006  isgrp2d  26044  nmobndseqi  26501  hhcmpl  26934  shne0i  27182  nmcopexi  27761  nmcfnexi  27785  cdj3lem3b  28174  rexcom4f  28192  iunin1f  28249  disjunsn  28281  ofpreima  28343  fpwrelmapffslem  28392  tosglblem  28505  xrnarchi  28575  ordtconlem1  28804  lmdvg  28833  esumfsup  28965  bnj168  29610  bnj1185  29677  bnj1542  29740  bnj865  29806  bnj916  29816  bnj983  29834  bnj1176  29886  bnj1189  29890  bnj1296  29902  bnj1398  29915  bnj1450  29931  bnj1463  29936  cvmliftlem15  30093  cvmlift2lem12  30109  dffr5  30464  dfon2lem9  30508  soseq  30563  noseponlem  30626  nosepon  30627  nodenselem4  30644  nodenselem5  30645  nofulllem5  30666  brbigcup  30736  elfuns  30753  brimage  30764  brimg  30775  dfrecs2  30788  imagesset  30791  brub  30792  brsegle  30946  gtinf  31046  filnetlem4  31108  bj-rexcom4a  31547  bj-rexcom4bv  31548  bj-rexcom4b  31549  bj-elsngl  31632  bj-mpt2mptALT  31701  iundif1  31991  poimirlem1  32005  poimirlem30  32034  poimirlem32  32036  poimir  32037  ismblfin  32045  volsupnfl  32049  itg2addnclem3  32059  fdc  32138  isfldidl  32365  prtlem10  32501  prter2  32517  islshpat  32654  lshpsmreu  32746  2dim  33106  islpln5  33171  lplnexatN  33199  islvol5  33215  dalem18  33317  dalem20  33329  lhpexle2  33646  lhpexle3  33648  lhpex2leN  33649  4atex2  33713  4atex2-0bOLDN  33715  cdlemftr3  34203  cdlemg17pq  34310  cdlemg19  34322  cdlemg21  34324  cdlemg33d  34347  dva1dim  34623  dih1dimatlem  34968  dihglb2  34981  dvh2dim  35084  mapdrvallem2  35284  mapdpglem3  35314  hdmapglem7a  35569  elrfirn  35608  isnacs2  35619  isnacs3  35623  sbc2rex  35701  4rexfrabdioph  35712  eldioph4b  35725  fphpd  35730  fiphp3d  35733  rencldnfilem  35734  rmxdioph  35942  expdiophlem1  35947  islnm2  36007  phisum  36147  elimaint  36311  cnviun  36313  imaiun1  36314  coiun1  36315  elintima  36316  briunov2  36345  prmunb2  36729  zfregs2VD  37300  evth2f  37399  evthf  37411  ndisj2  37448  stoweidlem28  38000  fourierdlem63  38145  fourierdlem65  38147  fourierdlem89  38171  fourierdlem90  38172  fourierdlem91  38173  fourierdlem100  38182  sge0pnfmpt  38401  ovn0  38506  2rexsb  38736  2rexrsb  38737  cbvrex2  38739  2reu5a  38743  n0snor2el  39143  usgr2edg1  39456  nbgrsym  39601  isuvtxa  39631  usgra2pth0  40177  usgvincvad  40224  usgvincvadALT  40227  usg2edgneu  40232  copisnmnd  40317  pgrpgt2nabl  40659  islindeps  40754  lindslinindsimp1  40758  lindslinindsimp2  40764  islindeps2  40784  islininds2  40785  isldepslvec2  40786  ldepslinc  40810
  Copyright terms: Public domain W3C validator