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

Theorem ralun 3370
Description: Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
ralun  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  B  ph )  ->  A. x  e.  ( A  u.  B
) ph )

Proof of Theorem ralun
StepHypRef Expression
1 ralunb 3369 . 2  |-  ( A. x  e.  ( A  u.  B ) ph  <->  ( A. x  e.  A  ph  /\  A. x  e.  B  ph ) )
21biimpri 197 1  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  B  ph )  ->  A. x  e.  ( A  u.  B
) ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wral 2556    u. cun 3163
This theorem is referenced by:  ac6sfi  7117  frfi  7118  fpwwe2lem13  8280  drsdirfi  14088  lbsextlem4  15930  fbun  17551  filcon  17594  cnmpt2pc  18442  chtub  20467  prsiga  23507  eupap1  23915  basexre  25625  ralunOLD  26445  kelac1  27264
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator