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

Theorem r19.42v 2865
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 2863 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 448 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2730 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 448 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 277 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-rex 2711
This theorem is referenced by:  ceqsrexbv  3083  ceqsrex2v  3084  2reuswap  3150  2reu5  3156  iunrab  4205  iunin2  4222  iundif2  4225  reusv2lem4  4484  iunopab  4611  elxp2  4845  cnvuni  5013  xpdifid  5254  elunirnALT  5957  f1oiso  6029  oprabrexex2  6556  oeeu  7030  trcl  7936  dfac5lem2  8282  axgroth4  8987  rexuz2  10894  4fvwrd4  11517  cshwsexa  12442  divalglem10  13589  divalgb  13591  lsmelval2  17088  tgcmp  18846  hauscmplem  18851  xkobval  19001  txtube  19055  txcmplem1  19056  txkgen  19067  xkococnlem  19074  mbfaddlem  20980  mbfsup  20984  elaa  21667  dchrisumlem3  22625  ax5seg  23007  sumdmdii  25642  2reuswap2  25696  unipreima  25785  fpwrelmapffslem  25857  esumfsup  26373  cvmliftlem15  27035  dfpo2  27412  ellines  28030  cnambfre  28284  rexrabdioph  28977  rmxdioph  29210  expdiophlem1  29215  2rmoswap  29854  rabasiun  30076  usgra2pth0  30148  usg2spot2nb  30504  usgreg2spot  30506  islindeps2  30747  isldepslvec2  30749  bnj168  31444  bnj1398  31748  bj-elsngl  32065  islshpat  32256  lfl1dim  32360  glbconxN  32616  3dim0  32695  2dim  32708  1dimN  32709  islpln5  32773  islvol5  32817  dalem20  32931  lhpex2leN  33251  mapdval4N  34871
  Copyright terms: Public domain W3C validator