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

Theorem r19.29r 2659
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 2658 . 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 2543 . 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 2518   E.wrex 2519
This theorem is referenced by:  2reu5  2948  rlimuni  11989  rlimno1  12092  neindisj2  16822  lmss  16988  fclsbas  17678  isfcf  17691  metcnp3  18048  bndth  18418  ellimc3  19191  cmptdst  24935  cover2  25725  bnj517  27966
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  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-ral 2523  df-rex 2524
  Copyright terms: Public domain W3C validator