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

Theorem r19.42v 2695
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 2694 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 437 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2569 . 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 2545
This theorem is referenced by:  ceqsrexbv  2903  ceqsrex2v  2904  2reuswap  2968  2reu5  2974  iunrab  3950  iunin2  3967  iundif2  3970  iunopab  4295  reusv2lem4  4537  elxp2  4706  cnvuni  4865  elunirnALT  5741  f1oiso  5810  oprabrexex2  5925  oeeu  6597  trcl  7406  dfac5lem2  7747  axgroth4  8450  rexuz2  10266  divalglem10  12597  divalgb  12599  lsmelval2  15834  tgcmp  17124  hauscmplem  17129  xkobval  17277  txtube  17330  txcmplem1  17331  txkgen  17342  xkococnlem  17349  mbfaddlem  19011  mbfsup  19015  elaa  19692  dchrisumlem3  20636  sumdmdii  22991  cvmliftlem15  23236  dfpo2  23518  ax5seg  23976  ellines  24185  rexrabdioph  26286  rmxdioph  26520  expdiophlem1  26525  2rmoswap  27353  bnj168  28037  bnj1398  28343  islshpat  28486  lfl1dim  28590  glbconxN  28846  3dim0  28925  2dim  28938  1dimN  28939  islpln5  29003  islvol5  29047  dalem20  29161  lhpex2leN  29481  mapdval4N  31101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-rex 2550
  Copyright terms: Public domain W3C validator