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

Theorem r19.42v 2707
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 2706 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 437 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2581 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 437 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 268 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wrex 2557
This theorem is referenced by:  ceqsrexbv  2915  ceqsrex2v  2916  2reuswap  2980  2reu5  2986  iunrab  3965  iunin2  3982  iundif2  3985  iunopab  4312  reusv2lem4  4554  elxp2  4723  cnvuni  4882  elunirnALT  5795  f1oiso  5864  oprabrexex2  5979  oeeu  6617  trcl  7426  dfac5lem2  7767  axgroth4  8470  rexuz2  10286  divalglem10  12617  divalgb  12619  lsmelval2  15854  tgcmp  17144  hauscmplem  17149  xkobval  17297  txtube  17350  txcmplem1  17351  txkgen  17362  xkococnlem  17369  mbfaddlem  19031  mbfsup  19035  elaa  19712  dchrisumlem3  20656  sumdmdii  23011  2reuswap2  23153  unipreima  23224  cvmliftlem15  23844  dfpo2  24183  elfuns  24525  ax5seg  24638  ellines  24847  rexrabdioph  26978  rmxdioph  27212  expdiophlem1  27217  2rmoswap  28065  4fvwrd4  28220  bnj168  29074  bnj1398  29380  islshpat  29829  lfl1dim  29933  glbconxN  30189  3dim0  30268  2dim  30281  1dimN  30282  islpln5  30346  islvol5  30390  dalem20  30504  lhpex2leN  30824  mapdval4N  32444
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-6 1715  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