| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ralunb | Structured version Visualization version GIF version | ||
| Description: Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
| Ref | Expression |
|---|---|
| ralunb | ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elunant 4184 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑))) | |
| 2 | 1 | albii 1819 | . . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑))) |
| 3 | 19.26 1870 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))) | |
| 4 | 2, 3 | bitri 275 | . 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))) |
| 5 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑)) | |
| 6 | df-ral 3062 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 7 | df-ral 3062 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
| 8 | 6, 7 | anbi12i 628 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))) |
| 9 | 4, 5, 8 | 3bitr4i 303 | 1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 ∈ wcel 2108 ∀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: ralun 4198 raldifeq 4494 ralprgf 4694 ralprg 4696 raltpg 4698 ralunsn 4894 disjxun 5141 naddunif 8731 undifixp 8974 ixpfi2 9390 dffi3 9471 fseqenlem1 10064 hashf1lem1 14494 pfxsuffeqwrdeq 14736 rexfiuz 15386 modfsummods 15829 modfsummod 15830 coprmproddvdslem 16699 prmind2 16722 prmreclem2 16955 lubun 18560 efgsp1 19755 unocv 21698 coe1fzgsumdlem 22307 evl1gsumdlem 22360 basdif0 22960 isclo 23095 ordtrest2 23212 ptbasfi 23589 ptcnplem 23629 ptrescn 23647 ordthmeolem 23809 prdsxmetlem 24378 prdsbl 24504 iblcnlem1 25823 ellimc2 25912 rlimcnp 27008 xrlimcnp 27011 ftalem3 27118 dchreq 27302 2sqlem10 27472 dchrisum0flb 27554 pntpbnd1 27630 addsuniflem 28034 mulsuniflem 28175 wlkp1lem8 29698 pthdlem1 29786 crctcshwlkn0lem7 29836 wwlksnext 29913 clwwlkccatlem 30008 clwwlkel 30065 clwwlkwwlksb 30073 wwlksext2clwwlk 30076 clwwlknonex2lem2 30127 3wlkdlem4 30181 3pthdlem1 30183 upgr4cycl4dv4e 30204 dfconngr1 30207 cntzun 33071 ordtrest2NEW 33922 subfacp1lem3 35187 subfacp1lem5 35189 erdszelem8 35203 hfext 36184 bj-raldifsn 37101 finixpnum 37612 lindsadd 37620 lindsenlbs 37622 poimirlem26 37653 poimirlem27 37654 poimirlem32 37659 prdsbnd 37800 rrnequiv 37842 hdmap14lem13 41882 usgrexmpl1lem 47980 usgrexmpl2lem 47985 usgrexmpl2trifr 47996 |
| Copyright terms: Public domain | W3C validator |