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

Theorem r19.42v 2696
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 2695 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 437 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2570 . 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 2546
This theorem is referenced by:  ceqsrexbv  2904  ceqsrex2v  2905  2reuswap  2969  2reu5  2975  iunrab  3951  iunin2  3968  iundif2  3971  iunopab  4298  reusv2lem4  4540  elxp2  4709  cnvuni  4868  elunirnALT  5781  f1oiso  5850  oprabrexex2  5965  oeeu  6603  trcl  7412  dfac5lem2  7753  axgroth4  8456  rexuz2  10272  divalglem10  12603  divalgb  12605  lsmelval2  15840  tgcmp  17130  hauscmplem  17135  xkobval  17283  txtube  17336  txcmplem1  17337  txkgen  17348  xkococnlem  17355  mbfaddlem  19017  mbfsup  19021  elaa  19698  dchrisumlem3  20642  sumdmdii  22997  2reuswap2  23139  unipreima  23211  cvmliftlem15  23831  dfpo2  24114  elfuns  24456  ax5seg  24568  ellines  24777  rexrabdioph  26886  rmxdioph  27120  expdiophlem1  27125  2rmoswap  27973  bnj168  28831  bnj1398  29137  islshpat  29280  lfl1dim  29384  glbconxN  29640  3dim0  29719  2dim  29732  1dimN  29733  islpln5  29797  islvol5  29841  dalem20  29955  lhpex2leN  30275  mapdval4N  31895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-rex 2551
  Copyright terms: Public domain W3C validator