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

Theorem r19.29r 2685
Description: Variation of Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
r19.29r  |-  ( ( E. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )

Proof of Theorem r19.29r
StepHypRef Expression
1 r19.29 2684 . 2  |-  ( ( A. x  e.  A  ps  /\  E. x  e.  A  ph )  ->  E. x  e.  A  ( ps  /\  ph )
)
2 ancom 439 . 2  |-  ( ( E. x  e.  A  ph 
/\  A. x  e.  A  ps )  <->  ( A. x  e.  A  ps  /\  E. x  e.  A  ph )
)
3 ancom 439 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
43rexbii 2569 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
51, 2, 43imtr4i 259 1  |-  ( ( E. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   A.wral 2544   E.wrex 2545
This theorem is referenced by:  2reu5  2974  rlimuni  12018  rlimno1  12121  neindisj2  16854  lmss  17020  fclsbas  17710  isfcf  17723  metcnp3  18080  bndth  18450  ellimc3  19223  cmptdst  24967  cover2  25757  bnj517  28184
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator