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

Theorem rexbii 2568
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.)
Hypothesis
Ref Expression
ralbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
rexbii  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )

Proof of Theorem rexbii
StepHypRef Expression
1 ralbii.1 . . . 4  |-  ( ph  <->  ps )
21a1i 10 . . 3  |-  (  T. 
->  ( ph  <->  ps )
)
32rexbidv 2564 . 2  |-  (  T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43trud 1314 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    T. wtru 1307   E.wrex 2544
This theorem is referenced by:  2rexbii  2570  rexanali  2589  r19.29r  2684  r19.42v  2694  r19.43  2695  rexcom13  2702  rexrot4  2703  3reeanv  2708  2ralor  2709  cbvrex2v  2773  rexcom4  2807  rexcom4a  2808  rexcom4b  2809  ceqsrex2v  2903  reu7  2960  0el  3471  uni0b  3852  iuncom  3911  iuncom4  3912  iuniin  3915  iunab  3948  iunn0  3962  iunin2  3966  iundif2  3969  iunun  3982  iunxiun  3984  iunpwss  3991  inuni  4173  iunopab  4296  dffr2  4358  frc  4359  frminex  4373  dfepfr  4378  epfrc  4379  sucel  4465  reusv2lem5  4539  reusv5OLD  4544  reusv7OLD  4546  reuxfrd  4559  iunpw  4570  xpiundi  4743  xpiundir  4744  reliin  4807  iunxpf  4832  cnvuni  4866  dmiun  4887  dfima3  5015  dffr3  5045  rniun  5091  dminxp  5118  imaco  5178  coiun  5182  isarep1  5331  rexrn  5667  ralrn  5668  fnasrn  5702  rexima  5757  ralima  5758  abrexco  5766  abrexex2g  5768  imaiun  5771  abrexex2  5780  fliftcnv  5810  rexrnmpt2  5959  rdglem1  6428  tz7.49  6457  oarec  6560  omeu  6583  qsid  6725  eroveu  6753  ixp0  6849  fimax2g  7103  marypha2lem2  7189  dfsup2  7195  dfsup2OLD  7196  dfoi  7226  wemapso2lem  7265  zfregcl  7308  zfreg  7309  zfreg2  7310  oemapso  7384  zfregs2  7415  infenaleph  7718  isinfcard  7719  kmlem7  7782  kmlem13  7788  fin23lem26  7951  dffin1-5  8014  fin12  8039  numth  8099  ac6n  8112  zorn2lem7  8129  zorng  8131  brdom7disj  8156  brdom6disj  8157  uniwun  8362  axgroth5  8446  axgroth4  8454  grothprim  8456  npomex  8620  genpass  8633  elreal  8753  dfinfmr  9731  infmsup  9732  infmrgelb  9734  infmrlb  9735  uzwo  10281  uzwoOLD  10282  ublbneg  10302  xrinfmss2  10629  rexanuz  11829  rexfiuz  11831  clim0  11980  incexc2  12297  divalglem10  12601  divalgb  12603  pythagtriplem2  12870  pythagtriplem19  12886  pythagtrip  12887  pceu  12899  prmreclem6  12968  4sqlem12  13003  imasaddfnlem  13430  isdrs2  14073  pgpfac1lem5  15314  dvdsrval  15427  opprunit  15443  lsmspsn  15837  lsmelval2  15838  islpidl  15998  tgval2  16694  ntreq0  16814  isclo2  16825  ist0-3  17073  tgcmp  17128  cmpfi  17135  is1stc2  17168  xkobval  17281  txtube  17334  txcmplem1  17335  xkococnlem  17353  eltsms  17815  metrest  18070  iscau3  18704  bcth  18751  pmltpc  18810  itg2i1fseq  19110  itg2cn  19118  plyun0  19579  aaliou3lem9  19730  1cubr  20138  dchrvmasumlema  20649  selbergsb  20724  ostth  20788  lpni  20846  isgrpo2  20864  isgrp2d  20902  nmobndseqi  21357  hhcmpl  21779  shne0i  22027  nmcopexi  22607  nmcfnexi  22631  cdj3lem3b  23020  rexcom4f  23134  r19.41vv  23163  xrofsup  23255  lmdvg  23376  cvmliftlem15  23829  cvmlift2lem12  23845  dfrtrclrec2  24040  dffr5  24110  dfon2lem9  24147  dffr4  24182  tz6.26  24205  soseq  24254  nodenselem4  24338  nodenselem5  24339  nofulllem5  24360  brbigcup  24438  elfuns  24454  brimage  24465  brimg  24476  tfrqfree  24489  brbtwn2  24533  colinearalg  24538  ax5seg  24566  axpasch  24569  axlowdimlem6  24575  axeuclidlem  24590  axeuclid  24591  brsegle  24731  negcmpprcal2  24946  dstr  25171  iscst4  25177  cbvprodi  25312  imtr  25398  sallnei  25529  intopcoaconb  25540  cnegvex2b  25662  rnegvex2b  25663  prismorcsetlem  25912  prismorcset  25914  dfiunv2  25916  gtinf  26234  nn0prpw  26239  filnetlem4  26330  fdc  26455  smprngopr  26677  isfldidl  26693  prtlem10  26733  prter2  26749  elrfirn  26770  isnacs2  26781  isnacs3  26785  4rexfrabdioph  26879  eldioph4b  26894  fphpd  26899  fiphp3d  26902  rencldnfilem  26903  rmxdioph  27109  expdiophlem1  27114  islnm2  27176  phisum  27518  evth2f  27686  evthf  27698  stoweidlem14  27763  stoweidlem28  27777  2rexsb  27948  2rexrsb  27949  cbvrex2  27951  2reu5a  27955  zfregs2VD  28617  bnj168  28758  bnj1185  28826  bnj1542  28889  bnj865  28955  bnj882  28958  bnj916  28965  bnj983  28983  bnj1176  29035  bnj1189  29039  bnj1296  29051  bnj1398  29064  bnj1450  29080  bnj1463  29085  islshpat  29207  lshpsmreu  29299  2dim  29659  islpln5  29724  lplnexatN  29752  islvol5  29768  dalem18  29870  dalem20  29882  lhpexle2  30199  lhpexle3  30201  lhpex2leN  30202  4atex2  30266  4atex2-0bOLDN  30268  cdlemftr3  30754  cdlemg17pq  30861  cdlemg19  30873  cdlemg21  30875  cdlemg33d  30898  dva1dim  31174  dih1dimatlem  31519  dihglb2  31532  dvh2dim  31635  mapdrvallem2  31835  mapdpglem3  31865  hdmapglem7a  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-rex 2549
  Copyright terms: Public domain W3C validator