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

Theorem r19.42v 2878
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 2876 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 450 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2743 . 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 2719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-rex 2724
This theorem is referenced by:  ceqsrexbv  3097  ceqsrex2v  3098  2reuswap  3164  2reu5  3170  iunrab  4220  iunin2  4237  iundif2  4240  reusv2lem4  4499  iunopab  4627  elxp2  4861  cnvuni  5029  xpdifid  5269  elunirn  5971  f1oiso  6045  oprabrexex2  6570  oeeu  7045  trcl  7951  dfac5lem2  8297  axgroth4  9002  rexuz2  10909  4fvwrd4  11536  cshwsexa  12461  divalglem10  13609  divalgb  13611  lsmelval2  17169  tgcmp  19007  hauscmplem  19012  xkobval  19162  txtube  19216  txcmplem1  19217  txkgen  19228  xkococnlem  19235  mbfaddlem  21141  mbfsup  21145  elaa  21785  dchrisumlem3  22743  ax5seg  23187  sumdmdii  25822  2reuswap2  25875  unipreima  25964  fpwrelmapffslem  26035  esumfsup  26522  cvmliftlem15  27190  dfpo2  27568  ellines  28186  cnambfre  28443  rexrabdioph  29135  rmxdioph  29368  expdiophlem1  29373  2rmoswap  30011  rabasiun  30233  usgra2pth0  30305  usg2spot2nb  30661  usgreg2spot  30663  islindeps2  31020  isldepslvec2  31022  bnj168  31724  bnj1398  32028  bj-elsngl  32464  islshpat  32665  lfl1dim  32769  glbconxN  33025  3dim0  33104  2dim  33117  1dimN  33118  islpln5  33182  islvol5  33226  dalem20  33340  lhpex2leN  33660  mapdval4N  35280
  Copyright terms: Public domain W3C validator