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

Theorem r19.42v 2694
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 2693 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 437 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2568 . 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 2544
This theorem is referenced by:  ceqsrexbv  2902  ceqsrex2v  2903  2reuswap  2967  2reu5  2973  iunrab  3949  iunin2  3966  iundif2  3969  iunopab  4296  reusv2lem4  4538  elxp2  4707  cnvuni  4866  elunirnALT  5779  f1oiso  5848  oprabrexex2  5963  oeeu  6601  trcl  7410  dfac5lem2  7751  axgroth4  8454  rexuz2  10270  divalglem10  12601  divalgb  12603  lsmelval2  15838  tgcmp  17128  hauscmplem  17133  xkobval  17281  txtube  17334  txcmplem1  17335  txkgen  17346  xkococnlem  17353  mbfaddlem  19015  mbfsup  19019  elaa  19696  dchrisumlem3  20640  sumdmdii  22995  2reuswap2  23137  unipreima  23209  cvmliftlem15  23829  dfpo2  24112  elfuns  24454  ax5seg  24566  ellines  24775  rexrabdioph  26875  rmxdioph  27109  expdiophlem1  27114  2rmoswap  27962  bnj168  28758  bnj1398  29064  islshpat  29207  lfl1dim  29311  glbconxN  29567  3dim0  29646  2dim  29659  1dimN  29660  islpln5  29724  islvol5  29768  dalem20  29882  lhpex2leN  30202  mapdval4N  31822
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 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-rex 2549
  Copyright terms: Public domain W3C validator