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

Theorem rexbii 2581
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 2577 . 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 2557
This theorem is referenced by:  2rexbii  2583  rexanali  2602  r19.29r  2697  r19.42v  2707  r19.43  2708  rexcom13  2715  rexrot4  2716  3reeanv  2721  2ralor  2722  cbvrex2v  2786  rexcom4  2820  rexcom4a  2821  rexcom4b  2822  ceqsrex2v  2916  reu7  2973  0el  3484  uni0b  3868  iuncom  3927  iuncom4  3928  iuniin  3931  iunab  3964  iunn0  3978  iunin2  3982  iundif2  3985  iunun  3998  iunxiun  4000  iunpwss  4007  inuni  4189  iunopab  4312  dffr2  4374  frc  4375  frminex  4389  dfepfr  4394  epfrc  4395  sucel  4481  reusv2lem5  4555  reusv5OLD  4560  reusv7OLD  4562  reuxfrd  4575  iunpw  4586  xpiundi  4759  xpiundir  4760  reliin  4823  iunxpf  4848  cnvuni  4882  dmiun  4903  dfima3  5031  dffr3  5061  rniun  5107  dminxp  5134  imaco  5194  coiun  5198  isarep1  5347  rexrn  5683  ralrn  5684  fnasrn  5718  rexima  5773  ralima  5774  abrexco  5782  abrexex2g  5784  imaiun  5787  abrexex2  5796  fliftcnv  5826  rexrnmpt2  5975  rdglem1  6444  tz7.49  6473  oarec  6576  omeu  6599  qsid  6741  eroveu  6769  ixp0  6865  fimax2g  7119  marypha2lem2  7205  dfsup2  7211  dfsup2OLD  7212  dfoi  7242  wemapso2lem  7281  zfregcl  7324  zfreg  7325  zfreg2  7326  oemapso  7400  zfregs2  7431  infenaleph  7734  isinfcard  7735  kmlem7  7798  kmlem13  7804  fin23lem26  7967  dffin1-5  8030  fin12  8055  numth  8115  ac6n  8128  zorn2lem7  8145  zorng  8147  brdom7disj  8172  brdom6disj  8173  uniwun  8378  axgroth5  8462  axgroth4  8470  grothprim  8472  npomex  8636  genpass  8649  elreal  8769  dfinfmr  9747  infmsup  9748  infmrgelb  9750  infmrlb  9751  uzwo  10297  uzwoOLD  10298  ublbneg  10318  xrinfmss2  10645  rexanuz  11845  rexfiuz  11847  clim0  11996  incexc2  12313  divalglem10  12617  divalgb  12619  pythagtriplem2  12886  pythagtriplem19  12902  pythagtrip  12903  pceu  12915  prmreclem6  12984  4sqlem12  13019  imasaddfnlem  13446  isdrs2  14089  pgpfac1lem5  15330  dvdsrval  15443  opprunit  15459  lsmspsn  15853  lsmelval2  15854  islpidl  16014  tgval2  16710  ntreq0  16830  isclo2  16841  ist0-3  17089  tgcmp  17144  cmpfi  17151  is1stc2  17184  xkobval  17297  txtube  17350  txcmplem1  17351  xkococnlem  17369  eltsms  17831  metrest  18086  iscau3  18720  bcth  18767  pmltpc  18826  itg2i1fseq  19126  itg2cn  19134  plyun0  19595  aaliou3lem9  19746  1cubr  20154  dchrvmasumlema  20665  selbergsb  20740  ostth  20804  lpni  20862  isgrpo2  20880  isgrp2d  20918  nmobndseqi  21373  hhcmpl  21795  shne0i  22043  nmcopexi  22623  nmcfnexi  22647  cdj3lem3b  23036  rexcom4f  23150  r19.41vv  23179  xrofsup  23270  lmdvg  23391  cvmliftlem15  23844  cvmlift2lem12  23860  dfrtrclrec2  24055  cbvcprod  24137  dffr5  24181  dfon2lem9  24218  dffr4  24253  tz6.26  24276  soseq  24325  nodenselem4  24409  nodenselem5  24410  nofulllem5  24431  brbigcup  24509  elfuns  24525  brimage  24536  brimg  24547  tfrqfree  24561  brbtwn2  24605  colinearalg  24610  ax5seg  24638  axpasch  24641  axlowdimlem6  24647  axeuclidlem  24662  axeuclid  24663  brsegle  24803  itg2addnc  25005  negcmpprcal2  25049  dstr  25274  iscst4  25280  cbvprodi  25415  imtr  25501  sallnei  25632  intopcoaconb  25643  cnegvex2b  25765  rnegvex2b  25766  prismorcsetlem  26015  prismorcset  26017  dfiunv2  26019  gtinf  26337  nn0prpw  26342  filnetlem4  26433  fdc  26558  smprngopr  26780  isfldidl  26796  prtlem10  26836  prter2  26852  elrfirn  26873  isnacs2  26884  isnacs3  26888  4rexfrabdioph  26982  eldioph4b  26997  fphpd  27002  fiphp3d  27005  rencldnfilem  27006  rmxdioph  27212  expdiophlem1  27217  islnm2  27279  phisum  27621  evth2f  27789  evthf  27801  stoweidlem14  27866  stoweidlem28  27880  2rexsb  28051  2rexrsb  28052  cbvrex2  28054  2reu5a  28058  4fvwrd4  28220  4cycl2vnunb  28439  zfregs2VD  28933  bnj168  29074  bnj1185  29142  bnj1542  29205  bnj865  29271  bnj882  29274  bnj916  29281  bnj983  29299  bnj1176  29351  bnj1189  29355  bnj1296  29367  bnj1398  29380  bnj1450  29396  bnj1463  29401  islshpat  29829  lshpsmreu  29921  2dim  30281  islpln5  30346  lplnexatN  30374  islvol5  30390  dalem18  30492  dalem20  30504  lhpexle2  30821  lhpexle3  30823  lhpex2leN  30824  4atex2  30888  4atex2-0bOLDN  30890  cdlemftr3  31376  cdlemg17pq  31483  cdlemg19  31495  cdlemg21  31497  cdlemg33d  31520  dva1dim  31796  dih1dimatlem  32141  dihglb2  32154  dvh2dim  32257  mapdrvallem2  32457  mapdpglem3  32487  hdmapglem7a  32742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-rex 2562
  Copyright terms: Public domain W3C validator