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

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

Proof of Theorem ralun
StepHypRef Expression
1 ralunb 4197 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
21biimpri 228 1 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) → ∀𝑥 ∈ (𝐴𝐵)𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wral 3061  cun 3949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-un 3956
This theorem is referenced by:  f1ounsn  7292  ac6sfi  9320  frfi  9321  fpwwe2lem12  10682  modfsummod  15830  drsdirfi  18351  lbsextlem4  21163  fbun  23848  filconn  23891  cnmpopc  24955  chtub  27256  prsiga  34132  finixpnum  37612  poimirlem31  37658  poimirlem32  37659  kelac1  43075  cantnfresb  43337
  Copyright terms: Public domain W3C validator