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

Theorem r19.29r 2857
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 2856 . 2  |-  ( ( A. x  e.  A  ps  /\  E. x  e.  A  ph )  ->  E. x  e.  A  ( ps  /\  ph )
)
2 ancom 450 . 2  |-  ( ( E. x  e.  A  ph 
/\  A. x  e.  A  ps )  <->  ( A. x  e.  A  ps  /\  E. x  e.  A  ph )
)
3 ancom 450 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
43rexbii 2739 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
51, 2, 43imtr4i 266 1  |-  ( ( E. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wral 2714   E.wrex 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-ral 2719  df-rex 2720
This theorem is referenced by:  r19.29imd  2858  r19.29af2  2859  2reu5  3166  rlimuni  13027  rlimno1  13130  neindisj2  18726  lmss  18901  fclsbas  19593  isfcf  19606  ucnima  19855  metcnp3  20114  cfilucfilOLD  20143  cfilucfil  20144  bndth  20529  ellimc3  21353  lmxrge0  26381  gsumesum  26509  esumcst  26513  esumfsup  26518  voliune  26644  volfiniune  26645  cover2  28605  bnj517  31876
  Copyright terms: Public domain W3C validator