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

Theorem rexbii 2691
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 2687 . 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 2667
This theorem is referenced by:  2rexbii  2693  rexanali  2712  r19.29r  2807  r19.42v  2822  r19.43  2823  rexcom13  2830  rexrot4  2831  3reeanv  2836  2ralor  2837  cbvrex2v  2901  rexcom4  2935  rexcom4a  2936  rexcom4b  2937  ceqsrex2v  3031  reu7  3089  0el  3604  uni0b  4000  iuncom  4059  iuncom4  4060  iuniin  4063  dfiunv2  4087  iunab  4097  iunn0  4111  iunin2  4115  iundif2  4118  iunun  4131  iunxiun  4133  iunpwss  4140  inuni  4322  iunopab  4446  dffr2  4507  frc  4508  frminex  4522  dfepfr  4527  epfrc  4528  sucel  4614  reusv2lem5  4687  reusv5OLD  4692  reusv7OLD  4694  reuxfrd  4707  iunpw  4718  xpiundi  4891  xpiundir  4892  reliin  4955  iunxpf  4980  cnvuni  5016  dmiun  5037  dfima3  5165  dffr3  5195  rniun  5241  dminxp  5270  imaco  5334  coiun  5338  isarep1  5491  rexrn  5831  ralrn  5832  elrnrexdmb  5834  fnasrn  5871  rexima  5936  ralima  5937  abrexco  5945  abrexex2g  5947  imaiun  5951  abrexex2  5960  fliftcnv  5992  rexrnmpt2  6144  rdglem1  6632  tz7.49  6661  oarec  6764  omeu  6787  qsid  6929  eroveu  6958  ixp0  7054  fimax2g  7312  marypha2lem2  7399  dfsup2  7405  dfsup2OLD  7406  dfoi  7436  wemapso2lem  7475  zfregcl  7518  zfreg  7519  zfreg2  7520  oemapso  7594  zfregs2  7625  infenaleph  7928  isinfcard  7929  kmlem7  7992  kmlem13  7998  fin23lem26  8161  dffin1-5  8224  fin12  8249  numth  8308  ac6n  8321  zorn2lem7  8338  zorng  8340  brdom7disj  8365  brdom6disj  8366  uniwun  8571  axgroth5  8655  axgroth4  8663  grothprim  8665  npomex  8829  genpass  8842  elreal  8962  dfinfmr  9941  infmsup  9942  infmrgelb  9944  infmrlb  9945  uzwo  10495  uzwoOLD  10496  ublbneg  10516  xrinfmss2  10845  4fvwrd4  11076  rexanuz  12104  rexfiuz  12106  clim0  12255  incexc2  12573  divalglem10  12877  divalgb  12879  pythagtriplem2  13146  pythagtriplem19  13162  pythagtrip  13163  pceu  13175  prmreclem6  13244  4sqlem12  13279  imasaddfnlem  13708  isdrs2  14351  pgpfac1lem5  15592  dvdsrval  15705  opprunit  15721  lsmspsn  16111  lsmelval2  16112  islpidl  16272  tgval2  16976  ntreq0  17096  isclo2  17107  neiptopnei  17151  ist0-3  17363  tgcmp  17418  cmpfi  17425  is1stc2  17458  xkobval  17571  txtube  17625  txcmplem1  17626  xkococnlem  17644  eltsms  18115  metrest  18507  iscau3  19184  bcth  19235  pmltpc  19300  itg2i1fseq  19600  itg2cn  19608  plyun0  20069  aaliou3lem9  20220  1cubr  20635  dchrvmasumlema  21147  selbergsb  21222  ostth  21286  usgra2edg1  21356  nbgraop1  21390  nbgraf1olem1  21404  lpni  21720  isgrpo2  21738  isgrp2d  21776  nmobndseqi  22233  hhcmpl  22655  shne0i  22903  nmcopexi  23483  nmcfnexi  23507  cdj3lem3b  23896  rexcom4f  23919  r19.41vv  23923  ofpreima  24034  tosglb  24145  xrnarchi  24207  lmdvg  24291  esumfsup  24413  cvmliftlem15  24938  cvmlift2lem12  24954  dfrtrclrec2  25096  cbvprod  25194  iprodmul  25269  dffr5  25324  dfon2lem9  25361  dffr4  25396  tz6.26  25419  soseq  25468  nodenselem4  25552  nodenselem5  25553  nofulllem5  25574  brbigcup  25652  elfuns  25668  brimage  25679  brimg  25690  tfrqfree  25704  brbtwn2  25748  colinearalg  25753  ax5seg  25781  axpasch  25784  axlowdimlem6  25790  axeuclidlem  25805  axeuclid  25806  brsegle  25946  ismblfin  26146  volsupnfl  26150  itg2addnclem3  26157  gtinf  26212  nn0prpw  26216  filnetlem4  26300  fdc  26339  smprngopr  26552  isfldidl  26568  prtlem10  26604  prter2  26620  elrfirn  26639  isnacs2  26650  isnacs3  26654  4rexfrabdioph  26748  eldioph4b  26762  fphpd  26767  fiphp3d  26770  rencldnfilem  26771  rmxdioph  26977  expdiophlem1  26982  islnm2  27044  phisum  27386  evth2f  27553  evthf  27565  stoweidlem28  27644  2rexsb  27815  2rexrsb  27816  cbvrex2  27818  2reu5a  27822  el2xptp  27948  usgra2pth0  28042  el2wlkonot  28066  el2spthonot  28067  el2wlkonotot0  28069  4cycl2vnunb  28121  vdn0frgrav2  28128  vdgn0frgrav2  28129  usg2spot2nb  28168  usgreg2spot  28170  zfregs2VD  28662  bnj168  28803  bnj1185  28871  bnj1542  28934  bnj865  29000  bnj916  29010  bnj983  29028  bnj1176  29080  bnj1189  29084  bnj1296  29096  bnj1398  29109  bnj1450  29125  bnj1463  29130  islshpat  29500  lshpsmreu  29592  2dim  29952  islpln5  30017  lplnexatN  30045  islvol5  30061  dalem18  30163  dalem20  30175  lhpexle2  30492  lhpexle3  30494  lhpex2leN  30495  4atex2  30559  4atex2-0bOLDN  30561  cdlemftr3  31047  cdlemg17pq  31154  cdlemg19  31166  cdlemg21  31168  cdlemg33d  31191  dva1dim  31467  dih1dimatlem  31812  dihglb2  31825  dvh2dim  31928  mapdrvallem2  32128  mapdpglem3  32158  hdmapglem7a  32413
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 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-rex 2672
  Copyright terms: Public domain W3C validator