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

Theorem r19.42v 3009
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 3007 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 450 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2958 . 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 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-rex 2813
This theorem is referenced by:  ceqsrexbv  3231  ceqsrex2v  3232  2reuswap  3299  2reu5  3305  rabasiun  4322  iunrab  4365  iunin2  4382  iundif2  4385  reusv2lem4  4644  iunopab  4776  elxp2  5010  cnvuni  5180  xpdifid  5426  elunirn  6142  f1oiso  6226  oprabrexex2  6764  oeeu  7242  trcl  8148  dfac5lem2  8494  axgroth4  9199  rexuz2  11121  4fvwrd4  11779  cshwsexa  12742  divalglem10  13908  divalgb  13910  lsmelval2  17507  tgcmp  19660  hauscmplem  19665  xkobval  19815  txtube  19869  txcmplem1  19870  txkgen  19881  xkococnlem  19888  mbfaddlem  21795  mbfsup  21799  elaa  22439  dchrisumlem3  23397  colperpexlem3  23804  mideu  23807  ax5seg  23910  usg2spot2nb  24728  usgreg2spot  24730  sumdmdii  26996  2reuswap2  27049  unipreima  27142  fpwrelmapffslem  27213  esumfsup  27702  cvmliftlem15  28369  dfpo2  28747  ellines  29365  cnambfre  29627  rexrabdioph  30318  rmxdioph  30551  expdiophlem1  30556  fourierdlem48  31410  2rmoswap  31611  usgra2pth0  31779  islindeps2  32032  isldepslvec2  32034  bnj168  32740  bnj1398  33044  bj-elsngl  33482  islshpat  33689  lfl1dim  33793  glbconxN  34049  3dim0  34128  2dim  34141  1dimN  34142  islpln5  34206  islvol5  34250  dalem20  34364  lhpex2leN  34684  mapdval4N  36304
  Copyright terms: Public domain W3C validator