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

Theorem r19.42v 2656
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 2655 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 439 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2532 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 439 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 270 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wrex 2510
This theorem is referenced by:  ceqsrexbv  2839  ceqsrex2v  2840  2reuswap  2902  iunrab  3847  iunin2  3864  iundif2  3867  iunopab  4189  reusv2lem4  4429  elxp2  4614  cnvuni  4773  elunirnALT  5631  f1oiso  5700  oprabrexex2  5815  oeeu  6487  trcl  7294  dfac5lem2  7635  axgroth4  8334  rexuz2  10149  divalglem10  12475  divalgb  12477  lsmelval2  15673  tgcmp  16960  hauscmplem  16965  xkobval  17113  txtube  17166  txcmplem1  17167  txkgen  17178  xkococnlem  17185  mbfaddlem  18847  mbfsup  18851  elaa  19528  dchrisumlem3  20472  sumdmdii  22825  cvmliftlem15  23000  dfpo2  23282  ax5seg  23740  ellines  23949  rexrabdioph  26041  rmxdioph  26275  expdiophlem1  26280  bnj168  27447  bnj1398  27753  islshpat  27896  lfl1dim  28000  glbconxN  28256  3dim0  28335  2dim  28348  1dimN  28349  islpln5  28413  islvol5  28457  dalem20  28571  lhpex2leN  28891  mapdval4N  30511
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-rex 2514
  Copyright terms: Public domain W3C validator