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

Theorem r19.42v 2998
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 2995 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 450 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2945 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 450 . 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 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-rex 2799
This theorem is referenced by:  ceqsrexbv  3220  ceqsrex2v  3221  2reuswap  3288  2reu5  3294  rabasiun  4319  iunrab  4362  iunin2  4379  iundif2  4382  reusv2lem4  4641  iunopab  4773  elxp2  5007  cnvuni  5179  xpdifid  5425  elunirn  6148  f1oiso  6232  oprabrexex2  6775  oeeu  7254  trcl  8162  dfac5lem2  8508  axgroth4  9213  rexuz2  11141  4fvwrd4  11801  cshwsexa  12771  divalglem10  13937  divalgb  13939  lsmelval2  17605  tgcmp  19774  hauscmplem  19779  unisngl  19901  xkobval  19960  txtube  20014  txcmplem1  20015  txkgen  20026  xkococnlem  20033  mbfaddlem  21940  mbfsup  21944  elaa  22584  dchrisumlem3  23548  colperpexlem3  23978  midex  23983  ax5seg  24113  usg2spot2nb  24937  usgreg2spot  24939  sumdmdii  27206  2reuswap2  27259  unipreima  27356  fpwrelmapffslem  27427  esumfsup  27949  cvmliftlem15  28616  dfpo2  29159  ellines  29777  cnambfre  30038  rexrabdioph  30702  rmxdioph  30933  expdiophlem1  30938  prmunb2  31167  fourierdlem48  31826  2rmoswap  32027  usgra2pth0  32193  islindeps2  32819  isldepslvec2  32821  bnj168  33518  bnj1398  33823  bj-elsngl  34274  islshpat  34482  lfl1dim  34586  glbconxN  34842  3dim0  34921  2dim  34934  1dimN  34935  islpln5  34999  islvol5  35043  dalem20  35157  lhpex2leN  35477  mapdval4N  37099
  Copyright terms: Public domain W3C validator