Theorem ralun 4221

Description: Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
ralun	⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑)

Proof of Theorem ralun

Step	Hyp	Ref	Expression
1		ralunb 4220	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))
2	1	biimpri 228	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3067   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-un 3981

This theorem is referenced by:  ac6sfi  9348  frfi  9349  fpwwe2lem12  10711  modfsummod  15842  drsdirfi  18375  lbsextlem4  21186  fbun  23869  filconn  23912  cnmpopc  24974  chtub  27274  prsiga  34095  finixpnum  37565  poimirlem31  37611  poimirlem32  37612  kelac1  43020  cantnfresb  43286