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

Theorem rexbii 2674
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 2670 . 2  |-  (  T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43trud 1329 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    T. wtru 1322   E.wrex 2650
This theorem is referenced by:  2rexbii  2676  rexanali  2695  r19.29r  2790  r19.42v  2805  r19.43  2806  rexcom13  2813  rexrot4  2814  3reeanv  2819  2ralor  2820  cbvrex2v  2884  rexcom4  2918  rexcom4a  2919  rexcom4b  2920  ceqsrex2v  3014  reu7  3072  0el  3587  uni0b  3982  iuncom  4041  iuncom4  4042  iuniin  4045  iunab  4078  iunn0  4092  iunin2  4096  iundif2  4099  iunun  4112  iunxiun  4114  iunpwss  4121  inuni  4303  iunopab  4427  dffr2  4488  frc  4489  frminex  4503  dfepfr  4508  epfrc  4509  sucel  4595  reusv2lem5  4668  reusv5OLD  4673  reusv7OLD  4675  reuxfrd  4688  iunpw  4699  xpiundi  4872  xpiundir  4873  reliin  4936  iunxpf  4961  cnvuni  4997  dmiun  5018  dfima3  5146  dffr3  5176  rniun  5222  dminxp  5251  imaco  5315  coiun  5319  isarep1  5472  rexrn  5811  ralrn  5812  elrnrexdmb  5814  fnasrn  5851  rexima  5916  ralima  5917  abrexco  5925  abrexex2g  5927  imaiun  5931  abrexex2  5940  fliftcnv  5972  rexrnmpt2  6124  rdglem1  6609  tz7.49  6638  oarec  6741  omeu  6764  qsid  6906  eroveu  6935  ixp0  7031  fimax2g  7289  marypha2lem2  7376  dfsup2  7382  dfsup2OLD  7383  dfoi  7413  wemapso2lem  7452  zfregcl  7495  zfreg  7496  zfreg2  7497  oemapso  7571  zfregs2  7602  infenaleph  7905  isinfcard  7906  kmlem7  7969  kmlem13  7975  fin23lem26  8138  dffin1-5  8201  fin12  8226  numth  8285  ac6n  8298  zorn2lem7  8315  zorng  8317  brdom7disj  8342  brdom6disj  8343  uniwun  8548  axgroth5  8632  axgroth4  8640  grothprim  8642  npomex  8806  genpass  8819  elreal  8939  dfinfmr  9917  infmsup  9918  infmrgelb  9920  infmrlb  9921  uzwo  10471  uzwoOLD  10472  ublbneg  10492  xrinfmss2  10821  4fvwrd4  11051  rexanuz  12076  rexfiuz  12078  clim0  12227  incexc2  12545  divalglem10  12849  divalgb  12851  pythagtriplem2  13118  pythagtriplem19  13134  pythagtrip  13135  pceu  13147  prmreclem6  13216  4sqlem12  13251  imasaddfnlem  13680  isdrs2  14323  pgpfac1lem5  15564  dvdsrval  15677  opprunit  15693  lsmspsn  16083  lsmelval2  16084  islpidl  16244  tgval2  16944  ntreq0  17064  isclo2  17075  neiptopnei  17119  ist0-3  17331  tgcmp  17386  cmpfi  17393  is1stc2  17426  xkobval  17539  txtube  17593  txcmplem1  17594  xkococnlem  17612  eltsms  18083  metrest  18444  iscau3  19102  bcth  19151  pmltpc  19214  itg2i1fseq  19514  itg2cn  19522  plyun0  19983  aaliou3lem9  20134  1cubr  20549  dchrvmasumlema  21061  selbergsb  21136  ostth  21200  usgra2edg1  21269  nbgraop1  21303  nbgraf1olem1  21317  lpni  21615  isgrpo2  21633  isgrp2d  21671  nmobndseqi  22128  hhcmpl  22550  shne0i  22798  nmcopexi  23378  nmcfnexi  23402  cdj3lem3b  23791  rexcom4f  23810  r19.41vv  23814  lmdvg  24142  esumfsup  24256  cvmliftlem15  24764  cvmlift2lem12  24780  dfrtrclrec2  24922  cbvprod  25020  iprodmul  25088  dffr5  25134  dfon2lem9  25171  dffr4  25206  tz6.26  25229  soseq  25278  nodenselem4  25362  nodenselem5  25363  nofulllem5  25384  brbigcup  25462  elfuns  25478  brimage  25489  brimg  25500  tfrqfree  25514  brbtwn2  25558  colinearalg  25563  ax5seg  25591  axpasch  25594  axlowdimlem6  25600  axeuclidlem  25615  axeuclid  25616  brsegle  25756  volsupnfl  25956  itg2addnc  25959  gtinf  26013  nn0prpw  26017  filnetlem4  26101  fdc  26140  smprngopr  26353  isfldidl  26369  prtlem10  26405  prter2  26421  elrfirn  26440  isnacs2  26451  isnacs3  26455  4rexfrabdioph  26549  eldioph4b  26563  fphpd  26568  fiphp3d  26571  rencldnfilem  26572  rmxdioph  26778  expdiophlem1  26783  islnm2  26845  phisum  27187  evth2f  27354  evthf  27366  stoweidlem28  27445  2rexsb  27616  2rexrsb  27617  cbvrex2  27619  2reu5a  27623  4cycl2vnunb  27770  vdn0frgrav2  27777  vdgn0frgrav2  27778  zfregs2VD  28294  bnj168  28435  bnj1185  28503  bnj1542  28566  bnj865  28632  bnj916  28642  bnj983  28660  bnj1176  28712  bnj1189  28716  bnj1296  28728  bnj1398  28741  bnj1450  28757  bnj1463  28762  islshpat  29132  lshpsmreu  29224  2dim  29584  islpln5  29649  lplnexatN  29677  islvol5  29693  dalem18  29795  dalem20  29807  lhpexle2  30124  lhpexle3  30126  lhpex2leN  30127  4atex2  30191  4atex2-0bOLDN  30193  cdlemftr3  30679  cdlemg17pq  30786  cdlemg19  30798  cdlemg21  30800  cdlemg33d  30823  dva1dim  31099  dih1dimatlem  31444  dihglb2  31457  dvh2dim  31560  mapdrvallem2  31760  mapdpglem3  31790  hdmapglem7a  32045
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-rex 2655
  Copyright terms: Public domain W3C validator