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  24180  dfon2lem9  24217  dffr4  24252  tz6.26  24275  soseq  24324  nodenselem4  24408  nodenselem5  24409  nofulllem5  24430  brbigcup  24508  elfuns  24524  brimage  24535  brimg  24546  tfrqfree  24560  brbtwn2  24604  colinearalg  24609  ax5seg  24637  axpasch  24640  axlowdimlem6  24646  axeuclidlem  24661  axeuclid  24662  brsegle  24802  itg2addnc  25004  negcmpprcal2  25048  dstr  25273  iscst4  25279  cbvprodi  25414  imtr  25500  sallnei  25631  intopcoaconb  25642  cnegvex2b  25764  rnegvex2b  25765  prismorcsetlem  26014  prismorcset  26016  dfiunv2  26018  gtinf  26336  nn0prpw  26341  filnetlem4  26432  fdc  26557  smprngopr  26779  isfldidl  26795  prtlem10  26835  prter2  26851  elrfirn  26872  isnacs2  26883  isnacs3  26887  4rexfrabdioph  26981  eldioph4b  26996  fphpd  27001  fiphp3d  27004  rencldnfilem  27005  rmxdioph  27211  expdiophlem1  27216  islnm2  27278  phisum  27620  evth2f  27788  evthf  27800  stoweidlem14  27865  stoweidlem28  27879  2rexsb  28050  2rexrsb  28051  cbvrex2  28053  2reu5a  28057  4fvwrd4  28219  4cycl2vnunb  28438  zfregs2VD  28932  bnj168  29073  bnj1185  29141  bnj1542  29204  bnj865  29270  bnj882  29273  bnj916  29280  bnj983  29298  bnj1176  29350  bnj1189  29354  bnj1296  29366  bnj1398  29379  bnj1450  29395  bnj1463  29400  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