| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ralun | Structured version Visualization version GIF version | ||
| Description: Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| Ref | Expression |
|---|---|
| ralun | ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralunb 4197 | . 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | |
| 2 | 1 | biimpri 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 |