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 2945
Description: Restricted quantifier version of 19.42v 1834 (see also 19.42 2052). (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 2942 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 452 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2889 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 452 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 281 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-rex 2743
This theorem is referenced by:  ceqsrexbv  3173  ceqsrex2v  3174  2reuswap  3242  2reu5  3248  rabasiun  4282  iunrab  4325  iunin2  4342  iundif2  4345  reusv2lem4  4607  iunopab  4737  elxp2  4852  cnvuni  5021  xpdifid  5265  elunirn  6156  f1oiso  6242  oprabrexex2  6783  oeeu  7304  trcl  8212  dfac5lem2  8555  axgroth4  9257  rexuz2  11210  4fvwrd4  11909  cshwsexa  12923  divalglem10  14383  divalgb  14385  lsmelval2  18308  tgcmp  20416  hauscmplem  20421  unisngl  20542  xkobval  20601  txtube  20655  txcmplem1  20656  txkgen  20667  xkococnlem  20674  mbfaddlem  22616  mbfsup  22620  elaa  23269  dchrisumlem3  24329  colperpexlem3  24774  midex  24779  iscgra1  24852  ax5seg  24968  usg2spot2nb  25793  usgreg2spot  25795  sumdmdii  28068  2reuswap2  28124  unipreima  28245  fpwrelmapffslem  28317  esumfsup  28891  bnj168  29538  bnj1398  29843  cvmliftlem15  30021  dfpo2  30395  ellines  30919  bj-elsngl  31562  bj-dfmpt2a  31630  ptrecube  31940  cnambfre  31989  islshpat  32583  lfl1dim  32687  glbconxN  32943  3dim0  33022  2dim  33035  1dimN  33036  islpln5  33100  islvol5  33144  dalem20  33258  lhpex2leN  33578  mapdval4N  35200  rexrabdioph  35637  rmxdioph  35871  expdiophlem1  35876  imaiun1  36243  coiun1  36244  prmunb2  36659  fourierdlem48  38018  2rmoswap  38605  wtgoldbnnsum4prm  38897  bgoldbnnsum3prm  38899  usgra2pth0  39722  islindeps2  40329  isldepslvec2  40331
  Copyright terms: Public domain W3C validator