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

Theorem r19.42v 2805
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 2804 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 438 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2674 . 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 2650
This theorem is referenced by:  ceqsrexbv  3013  ceqsrex2v  3014  2reuswap  3079  2reu5  3085  iunrab  4079  iunin2  4096  iundif2  4099  iunopab  4427  reusv2lem4  4667  elxp2  4836  cnvuni  4997  elunirnALT  5939  f1oiso  6010  oprabrexex2  6128  oeeu  6782  trcl  7597  dfac5lem2  7938  axgroth4  8640  rexuz2  10460  4fvwrd4  11051  divalglem10  12849  divalgb  12851  lsmelval2  16084  tgcmp  17386  hauscmplem  17391  xkobval  17539  txtube  17593  txcmplem1  17594  txkgen  17605  xkococnlem  17612  mbfaddlem  19419  mbfsup  19423  elaa  20100  dchrisumlem3  21052  sumdmdii  23766  2reuswap2  23819  unipreima  23898  esumfsup  24256  cvmliftlem15  24764  dfpo2  25136  elfuns  25478  ax5seg  25591  ellines  25800  rexrabdioph  26545  rmxdioph  26778  expdiophlem1  26783  2rmoswap  27630  bnj168  28435  bnj1398  28741  islshpat  29132  lfl1dim  29236  glbconxN  29492  3dim0  29571  2dim  29584  1dimN  29585  islpln5  29649  islvol5  29693  dalem20  29807  lhpex2leN  30127  mapdval4N  31747
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 2655
  Copyright terms: Public domain W3C validator