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

Theorem r19.42v 2798
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 2797 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 438 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2667 . 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 2643
This theorem is referenced by:  ceqsrexbv  3006  ceqsrex2v  3007  2reuswap  3072  2reu5  3078  iunrab  4072  iunin2  4089  iundif2  4092  iunopab  4420  reusv2lem4  4660  elxp2  4829  cnvuni  4990  elunirnALT  5932  f1oiso  6003  oprabrexex2  6121  oeeu  6775  trcl  7590  dfac5lem2  7931  axgroth4  8633  rexuz2  10453  4fvwrd4  11044  divalglem10  12842  divalgb  12844  lsmelval2  16077  tgcmp  17379  hauscmplem  17384  xkobval  17532  txtube  17586  txcmplem1  17587  txkgen  17598  xkococnlem  17605  mbfaddlem  19412  mbfsup  19416  elaa  20093  dchrisumlem3  21045  sumdmdii  23759  2reuswap2  23812  unipreima  23891  esumfsup  24249  cvmliftlem15  24757  dfpo2  25129  elfuns  25471  ax5seg  25584  ellines  25793  rexrabdioph  26538  rmxdioph  26771  expdiophlem1  26776  2rmoswap  27623  bnj168  28428  bnj1398  28734  islshpat  29183  lfl1dim  29287  glbconxN  29543  3dim0  29622  2dim  29635  1dimN  29636  islpln5  29700  islvol5  29744  dalem20  29858  lhpex2leN  30178  mapdval4N  31798
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 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-rex 2648
  Copyright terms: Public domain W3C validator