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

Theorem rexbii 2735
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 11 . . 3  |-  ( T. 
->  ( ph  <->  ps )
)
32rexbidv 2731 . 2  |-  ( T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43trud 1378 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1370   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-rex 2716
This theorem is referenced by:  2rexbii  2737  rexanali  2756  r19.29r  2853  r19.29imd  2854  r19.41vv  2869  r19.42v  2870  r19.43  2871  rexcom13  2878  rexrot4  2879  3reeanv  2884  2ralor  2885  cbvrex2v  2951  rexcom4  2987  rexcom4a  2988  rexcom4b  2989  ceqsrex2v  3090  reu7  3149  0el  3649  uni0b  4111  iuncom  4172  iuncom4  4173  iuniin  4176  dfiunv2  4201  iunab  4211  iunn0  4225  iunin2  4229  iundif2  4232  iunun  4246  iunxiun  4248  iunpwss  4255  inuni  4449  reusv2lem5  4492  reusv5OLD  4497  reusv7OLD  4499  reuxfrd  4512  iunopab  4619  dffr2  4680  frc  4681  frminex  4695  dfepfr  4700  epfrc  4701  sucel  4787  xpiundi  4888  xpiundir  4889  reliin  4956  iunxpf  4983  cnvuni  5021  dmiun  5043  dfima3  5167  dffr3  5196  rniun  5242  xpdifid  5261  dminxp  5273  imaco  5338  coiun  5342  isarep1  5492  rexrn  5840  ralrn  5841  elrnrexdmb  5843  fnasrn  5883  rexima  5951  ralima  5952  abrexco  5956  imaiun  5957  fliftcnv  5999  rexrnmpt2  6201  iunpw  6385  abrexex2g  6549  abrexex2  6553  rdglem1  6863  tz7.49  6892  oarec  6993  omeu  7016  qsid  7158  eroveu  7187  ixp0  7288  fimax2g  7550  marypha2lem2  7678  dfsup2  7684  dfsup2OLD  7685  dfoi  7717  wemapsolem  7756  zfregcl  7801  zfreg  7802  zfreg2  7803  oemapso  7882  zfregs2  7945  infenaleph  8253  isinfcard  8254  kmlem7  8317  kmlem13  8323  fin23lem26  8486  dffin1-5  8549  fin12  8574  numth  8633  ac6n  8646  zorn2lem7  8663  zorng  8665  brdom7disj  8690  brdom6disj  8691  uniwun  8899  axgroth5  8983  axgroth4  8991  grothprim  8993  npomex  9157  genpass  9170  elreal  9290  dfinfmr  10299  infmsup  10300  infmrgelb  10302  infmrlb  10303  uzwo  10909  uzwoOLD  10910  ublbneg  10931  xrinfmss2  11265  4fvwrd4  11525  hashge2el2dif  12176  rexanuz  12825  rexfiuz  12827  clim0  12976  cbvsum  13164  incexc2  13293  divalglem10  13598  divalgb  13600  pythagtriplem2  13876  pythagtriplem19  13892  pythagtrip  13893  pceu  13905  prmreclem6  13974  4sqlem12  14009  cshwshashlem1  14114  cshwshash  14123  imasaddfnlem  14458  isdrs2  15101  symgmov1  15888  symgmov2  15889  pmtrprfvalrn  15985  pgpfac1lem5  16570  dvdsrval  16727  opprunit  16743  lsmspsn  17145  lsmelval2  17146  islpidl  17308  mdetunilem8  18405  tgval2  18541  ntreq0  18661  isclo2  18672  neiptopnei  18716  ist0-3  18929  tgcmp  18984  cmpfi  18991  is1stc2  19026  xkobval  19139  txtube  19193  txcmplem1  19194  xkococnlem  19212  eltsms  19683  metrest  20079  iscau3  20769  bcth  20820  pmltpc  20914  itg2i1fseq  21213  itg2cn  21221  plyun0  21645  aaliou3lem9  21796  1cubr  22217  dchrvmasumlema  22729  selbergsb  22804  ostth  22868  tglowdim1i  22934  legtrid  23002  brbtwn2  23119  colinearalg  23124  ax5seg  23152  axpasch  23155  axlowdimlem6  23161  axeuclidlem  23176  axeuclid  23177  usgra2edg1  23270  nbgraop1  23304  nbgraf1olem1  23318  lpni  23634  isgrpo2  23652  isgrp2d  23690  nmobndseqi  24147  hhcmpl  24570  shne0i  24819  nmcopexi  25399  nmcfnexi  25423  cdj3lem3b  25812  rexcom4f  25829  disjunsn  25904  ofpreima  25952  fpwrelmapffslem  26000  tosglblem  26098  xrnarchi  26169  archiabl  26183  ordtconlem1  26323  lmdvg  26352  esumfsup  26488  cvmliftlem15  27156  cvmlift2lem12  27172  dfrtrclrec2  27314  cbvprod  27397  iprodmul  27472  dffr5  27532  dfon2lem9  27573  dffr4  27612  tz6.26  27635  soseq  27684  nodenselem4  27794  nodenselem5  27795  nofulllem5  27816  brbigcup  27898  elfuns  27915  brimage  27926  brimg  27937  tfrqfree  27951  imagesset  27953  brub  27954  brsegle  28108  iundif1  28384  ismblfin  28403  volsupnfl  28407  itg2addnclem3  28416  gtinf  28485  nn0prpw  28489  filnetlem4  28573  fdc  28612  smprngopr  28823  isfldidl  28839  prtlem10  28981  prter2  28997  elrfirn  29002  isnacs2  29013  isnacs3  29017  sbc2rex  29096  4rexfrabdioph  29107  eldioph4b  29121  fphpd  29126  fiphp3d  29129  rencldnfilem  29130  rmxdioph  29336  expdiophlem1  29341  islnm2  29402  phisum  29538  evth2f  29708  evthf  29720  stoweidlem28  29794  2rexsb  29965  2rexrsb  29966  cbvrex2  29968  2reu5a  29972  el2xptp  30097  rabasiun  30201  wrdlen1  30221  usgra2pth0  30273  el2wlkonot  30359  el2spthonot  30360  el2wlkonotot0  30362  4cycl2vnunb  30580  vdn0frgrav2  30587  vdgn0frgrav2  30588  usg2spot2nb  30629  usgreg2spot  30631  numclwwlkun  30643  pgrpgt2nabel  30738  fsuppmapnn0ub  30765  fsuppmapnn0fiubex  30769  mat1dimelbas  30827  mat1dimbas  30828  pmatcollpw2lem  30862  islindeps  30918  lindslinindsimp1  30922  lindslinindsimp2  30928  islindeps2  30948  islininds2  30949  isldepslvec2  30950  ldepslinc  30982  zfregs2VD  31506  bnj168  31650  bnj1185  31716  bnj1542  31779  bnj865  31845  bnj916  31855  bnj983  31873  bnj1176  31925  bnj1189  31929  bnj1296  31941  bnj1398  31954  bnj1450  31970  bnj1463  31975  bj-rexcom4a  32281  bj-rexcom4bv  32282  bj-rexcom4b  32283  bj-elsngl  32361  islshpat  32555  lshpsmreu  32647  2dim  33007  islpln5  33072  lplnexatN  33100  islvol5  33116  dalem18  33218  dalem20  33230  lhpexle2  33547  lhpexle3  33549  lhpex2leN  33550  4atex2  33614  4atex2-0bOLDN  33616  cdlemftr3  34102  cdlemg17pq  34209  cdlemg19  34221  cdlemg21  34223  cdlemg33d  34246  dva1dim  34522  dih1dimatlem  34867  dihglb2  34880  dvh2dim  34983  mapdrvallem2  35183  mapdpglem3  35213  hdmapglem7a  35468
  Copyright terms: Public domain W3C validator