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

Theorem r19.42v 2931
Description: Restricted quantifier version of 19.42v 1842 (see also 19.42 2071). (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 2928 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 457 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2881 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 457 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 285 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-rex 2762
This theorem is referenced by:  ceqsrexbv  3161  ceqsrex2v  3162  2reuswap  3230  2reu5  3236  rabasiun  4273  iunrab  4316  iunin2  4333  iundif2  4336  reusv2lem4  4605  iunopab  4737  elxp2  4857  cnvuni  5026  xpdifid  5271  elunirn  6174  f1oiso  6260  oprabrexex2  6802  oeeu  7322  trcl  8230  dfac5lem2  8573  axgroth4  9275  rexuz2  11233  4fvwrd4  11936  cshwsexa  12980  divalglem10  14462  divalgb  14464  lsmelval2  18386  tgcmp  20493  hauscmplem  20498  unisngl  20619  xkobval  20678  txtube  20732  txcmplem1  20733  txkgen  20744  xkococnlem  20751  mbfaddlem  22695  mbfsup  22699  elaa  23348  dchrisumlem3  24408  colperpexlem3  24853  midex  24858  iscgra1  24931  ax5seg  25047  usg2spot2nb  25872  usgreg2spot  25874  sumdmdii  28149  2reuswap2  28203  unipreima  28321  fpwrelmapffslem  28392  esumfsup  28965  bnj168  29610  bnj1398  29915  cvmliftlem15  30093  dfpo2  30466  ellines  30990  bj-elsngl  31632  bj-dfmpt2a  31700  ptrecube  32004  cnambfre  32053  islshpat  32654  lfl1dim  32758  glbconxN  33014  3dim0  33093  2dim  33106  1dimN  33107  islpln5  33171  islvol5  33215  dalem20  33329  lhpex2leN  33649  mapdval4N  35271  rexrabdioph  35708  rmxdioph  35942  expdiophlem1  35947  imaiun1  36314  coiun1  36315  prmunb2  36729  fourierdlem48  38130  2rmoswap  38750  wtgoldbnnsum4prm  39042  bgoldbnnsum3prm  39044  usgra2pth0  40177  islindeps2  40784  isldepslvec2  40786
  Copyright terms: Public domain W3C validator