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

Theorem r19.42v 2983
Description: Restricted quantifier version of 19.42v 1823 (see also 19.42 2027). (Contributed by NM, 27-May-1998.)
Assertion
Ref Expression
r19.42v  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem r19.42v
StepHypRef Expression
1 r19.41v 2980 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 451 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2927 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 451 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 280 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-rex 2781
This theorem is referenced by:  ceqsrexbv  3206  ceqsrex2v  3207  2reuswap  3274  2reu5  3280  rabasiun  4300  iunrab  4343  iunin2  4360  iundif2  4363  reusv2lem4  4625  iunopab  4753  elxp2  4868  cnvuni  5037  xpdifid  5281  elunirn  6168  f1oiso  6254  oprabrexex2  6794  oeeu  7309  trcl  8214  dfac5lem2  8556  axgroth4  9258  rexuz2  11211  4fvwrd4  11910  cshwsexa  12914  divalglem10  14371  divalgb  14373  lsmelval2  18296  tgcmp  20403  hauscmplem  20408  unisngl  20529  xkobval  20588  txtube  20642  txcmplem1  20643  txkgen  20654  xkococnlem  20661  mbfaddlem  22603  mbfsup  22607  elaa  23256  dchrisumlem3  24316  colperpexlem3  24761  midex  24766  iscgra1  24839  ax5seg  24955  usg2spot2nb  25779  usgreg2spot  25781  sumdmdii  28054  2reuswap2  28110  unipreima  28235  fpwrelmapffslem  28311  esumfsup  28887  bnj168  29534  bnj1398  29839  cvmliftlem15  30017  dfpo2  30390  ellines  30912  bj-elsngl  31518  ptrecube  31854  cnambfre  31903  islshpat  32502  lfl1dim  32606  glbconxN  32862  3dim0  32941  2dim  32954  1dimN  32955  islpln5  33019  islvol5  33063  dalem20  33177  lhpex2leN  33497  mapdval4N  35119  rexrabdioph  35556  rmxdioph  35791  expdiophlem1  35796  imaiun1  36103  coiun1  36104  prmunb2  36517  fourierdlem48  37838  2rmoswap  38318  wtgoldbnnsum4prm  38609  bgoldbnnsum3prm  38611  usgra2pth0  38941  islindeps2  39550  isldepslvec2  39552
  Copyright terms: Public domain W3C validator