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

Theorem r19.42v 2665
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 2664 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 439 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2539 . 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 2517
This theorem is referenced by:  ceqsrexbv  2853  ceqsrex2v  2854  2reuswap  2916  iunrab  3890  iunin2  3907  iundif2  3910  iunopab  4233  reusv2lem4  4475  elxp2  4660  cnvuni  4819  elunirnALT  5678  f1oiso  5747  oprabrexex2  5862  oeeu  6534  trcl  7343  dfac5lem2  7684  axgroth4  8387  rexuz2  10202  divalglem10  12528  divalgb  12530  lsmelval2  15765  tgcmp  17055  hauscmplem  17060  xkobval  17208  txtube  17261  txcmplem1  17262  txkgen  17273  xkococnlem  17280  mbfaddlem  18942  mbfsup  18946  elaa  19623  dchrisumlem3  20567  sumdmdii  22920  cvmliftlem15  23166  dfpo2  23448  ax5seg  23906  ellines  24115  rexrabdioph  26207  rmxdioph  26441  expdiophlem1  26446  bnj168  27770  bnj1398  28076  islshpat  28337  lfl1dim  28441  glbconxN  28697  3dim0  28776  2dim  28789  1dimN  28790  islpln5  28854  islvol5  28898  dalem20  29012  lhpex2leN  29332  mapdval4N  30952
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 2521
  Copyright terms: Public domain W3C validator