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

Theorem r19.42v 2854
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 2853 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 438 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2722 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 438 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 269 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wrex 2698
This theorem is referenced by:  ceqsrexbv  3062  ceqsrex2v  3063  2reuswap  3128  2reu5  3134  iunrab  4130  iunin2  4147  iundif2  4150  iunopab  4478  reusv2lem4  4719  elxp2  4888  cnvuni  5049  elunirnALT  5992  f1oiso  6063  oprabrexex2  6181  oeeu  6838  trcl  7656  dfac5lem2  7997  axgroth4  8699  rexuz2  10520  4fvwrd4  11113  divalglem10  12914  divalgb  12916  lsmelval2  16149  tgcmp  17456  hauscmplem  17461  xkobval  17610  txtube  17664  txcmplem1  17665  txkgen  17676  xkococnlem  17683  mbfaddlem  19544  mbfsup  19548  elaa  20225  dchrisumlem3  21177  sumdmdii  23910  2reuswap2  23967  unipreima  24048  esumfsup  24452  cvmliftlem15  24977  dfpo2  25370  ax5seg  25869  ellines  26078  cnambfre  26245  rexrabdioph  26835  rmxdioph  27068  expdiophlem1  27073  2rmoswap  27919  cshwsexa  28244  usgra2pth0  28255  usg2spot2nb  28381  usgreg2spot  28383  bnj168  29024  bnj1398  29330  islshpat  29742  lfl1dim  29846  glbconxN  30102  3dim0  30181  2dim  30194  1dimN  30195  islpln5  30259  islvol5  30303  dalem20  30417  lhpex2leN  30737  mapdval4N  32357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-rex 2703
  Copyright terms: Public domain W3C validator