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

Theorem r19.29r 2834
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 2833 . 2  |-  ( ( A. x  e.  A  ps  /\  E. x  e.  A  ph )  ->  E. x  e.  A  ( ps  /\  ph )
)
2 ancom 438 . 2  |-  ( ( E. x  e.  A  ph 
/\  A. x  e.  A  ps )  <->  ( A. x  e.  A  ps  /\  E. x  e.  A  ph )
)
3 ancom 438 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
43rexbii 2717 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
51, 2, 43imtr4i 258 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 4    /\ wa 359   A.wral 2692   E.wrex 2693
This theorem is referenced by:  r19.29af2  2835  2reu5  3129  rlimuni  12327  rlimno1  12430  neindisj2  17170  lmss  17345  fclsbas  18036  isfcf  18049  ucnima  18294  metcnp3  18553  cfilucfilOLD  18582  cfilucfil  18583  bndth  18966  ellimc3  19749  lmxrge0  24320  gsumesum  24434  esumcst  24438  esumfsup  24443  voliune  24568  volfiniune  24569  cover2  26347  bnj517  29008
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-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-ral 2697  df-rex 2698
  Copyright terms: Public domain W3C validator