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

Theorem r19.42v 2669
Description: Restricted version of Theorem 19.42 of [Margaris] p. 90. (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 2668 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 439 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2543 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 439 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 270 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wrex 2519
This theorem is referenced by:  ceqsrexbv  2877  ceqsrex2v  2878  2reuswap  2942  2reu5  2948  iunrab  3923  iunin2  3940  iundif2  3943  iunopab  4268  reusv2lem4  4510  elxp2  4695  cnvuni  4854  elunirnALT  5713  f1oiso  5782  oprabrexex2  5897  oeeu  6569  trcl  7378  dfac5lem2  7719  axgroth4  8422  rexuz2  10238  divalglem10  12564  divalgb  12566  lsmelval2  15801  tgcmp  17091  hauscmplem  17096  xkobval  17244  txtube  17297  txcmplem1  17298  txkgen  17309  xkococnlem  17316  mbfaddlem  18978  mbfsup  18982  elaa  19659  dchrisumlem3  20603  sumdmdii  22956  cvmliftlem15  23202  dfpo2  23484  ax5seg  23942  ellines  24151  rexrabdioph  26243  rmxdioph  26477  expdiophlem1  26482  2rmoswap  27311  bnj168  27890  bnj1398  28196  islshpat  28457  lfl1dim  28561  glbconxN  28817  3dim0  28896  2dim  28909  1dimN  28910  islpln5  28974  islvol5  29018  dalem20  29132  lhpex2leN  29452  mapdval4N  31072
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-rex 2524
  Copyright terms: Public domain W3C validator