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

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

Proof of Theorem ralun
StepHypRef Expression
1 ralunb 4096 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
21biimpri 231 1 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) → ∀𝑥 ∈ (𝐴𝐵)𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∀wral 3070   ∪ cun 3856 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-v 3411  df-un 3863 This theorem is referenced by:  ac6sfi  8795  frfi  8796  fpwwe2lem12  10102  modfsummod  15197  drsdirfi  17614  lbsextlem4  20001  fbun  22540  filconn  22583  cnmpopc  23629  chtub  25895  prsiga  31618  finixpnum  35344  poimirlem31  35390  poimirlem32  35391  kelac1  40402
 Copyright terms: Public domain W3C validator