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

Theorem ralun 3357
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 3356 . 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 2543    u. cun 3150
This theorem is referenced by:  ac6sfi  7101  frfi  7102  fpwwe2lem13  8264  drsdirfi  14072  lbsextlem4  15914  fbun  17535  filcon  17578  cnmpt2pc  18426  chtub  20451  prsiga  23492  eupap1  23900  basexre  25522  ralunOLD  26342  kelac1  27161
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator