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

Theorem ralun 3793
 Description: Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
ralun ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) → ∀𝑥 ∈ (𝐴𝐵)𝜑)

Proof of Theorem ralun
StepHypRef Expression
1 ralunb 3792 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
21biimpri 218 1 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) → ∀𝑥 ∈ (𝐴𝐵)𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384  ∀wral 2911   ∪ cun 3570 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-v 3200  df-un 3577 This theorem is referenced by:  ac6sfi  8201  frfi  8202  fpwwe2lem13  9461  modfsummod  14520  drsdirfi  16932  lbsextlem4  19155  fbun  21638  filconn  21681  cnmpt2pc  22721  chtub  24931  prsiga  30179  finixpnum  33374  poimirlem31  33420  poimirlem32  33421  kelac1  37459
 Copyright terms: Public domain W3C validator