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

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

Proof of Theorem ralun
StepHypRef Expression
1 ralunb 4138 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
21biimpri 227 1 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) → ∀𝑥 ∈ (𝐴𝐵)𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wral 3061  cun 3896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-v 3443  df-un 3903
This theorem is referenced by:  ac6sfi  9152  frfi  9153  fpwwe2lem12  10499  modfsummod  15605  drsdirfi  18120  lbsextlem4  20529  fbun  23097  filconn  23140  cnmpopc  24197  chtub  26466  prsiga  32397  finixpnum  35875  poimirlem31  35921  poimirlem32  35922  kelac1  41159
  Copyright terms: Public domain W3C validator