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

Theorem r19.42v 2830
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 2829 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 438 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2699 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 438 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 269 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wrex 2675
This theorem is referenced by:  ceqsrexbv  3038  ceqsrex2v  3039  2reuswap  3104  2reu5  3110  iunrab  4106  iunin2  4123  iundif2  4126  iunopab  4454  reusv2lem4  4694  elxp2  4863  cnvuni  5024  elunirnALT  5967  f1oiso  6038  oprabrexex2  6156  oeeu  6813  trcl  7628  dfac5lem2  7969  axgroth4  8671  rexuz2  10492  4fvwrd4  11084  divalglem10  12885  divalgb  12887  lsmelval2  16120  tgcmp  17426  hauscmplem  17431  xkobval  17579  txtube  17633  txcmplem1  17634  txkgen  17645  xkococnlem  17652  mbfaddlem  19513  mbfsup  19517  elaa  20194  dchrisumlem3  21146  sumdmdii  23879  2reuswap2  23936  unipreima  24017  esumfsup  24421  cvmliftlem15  24946  dfpo2  25334  elfuns  25676  ax5seg  25789  ellines  25998  cnambfre  26162  rexrabdioph  26752  rmxdioph  26985  expdiophlem1  26990  2rmoswap  27837  usgra2pth0  28050  usg2spot2nb  28176  usgreg2spot  28178  bnj168  28815  bnj1398  29121  islshpat  29512  lfl1dim  29616  glbconxN  29872  3dim0  29951  2dim  29964  1dimN  29965  islpln5  30029  islvol5  30073  dalem20  30187  lhpex2leN  30507  mapdval4N  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-rex 2680
  Copyright terms: Public domain W3C validator