![]() |
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 4176 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑))) | |
2 | 1 | albii 1813 | . . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑))) |
3 | 19.26 1865 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))) | |
4 | 2, 3 | bitri 274 | . 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))) |
5 | df-ral 3051 | . 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑)) | |
6 | df-ral 3051 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
7 | df-ral 3051 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
8 | 6, 7 | anbi12i 626 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))) |
9 | 4, 5, 8 | 3bitr4i 302 | 1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∀wal 1531 ∈ wcel 2098 ∀wral 3050 ∪ cun 3942 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-v 3463 df-un 3949 |
This theorem is referenced by: ralun 4190 raldifeq 4495 ralprgf 4698 ralprg 4700 raltpg 4704 ralunsn 4896 disjxun 5147 naddunif 8714 undifixp 8953 ixpfi2 9381 dffi3 9461 fseqenlem1 10054 hashf1lem1 14456 hashf1lem1OLD 14457 pfxsuffeqwrdeq 14689 rexfiuz 15335 modfsummods 15780 modfsummod 15781 coprmproddvdslem 16641 prmind2 16664 prmreclem2 16894 lubun 18515 efgsp1 19709 unocv 21634 coe1fzgsumdlem 22252 evl1gsumdlem 22305 basdif0 22905 isclo 23040 ordtrest2 23157 ptbasfi 23534 ptcnplem 23574 ptrescn 23592 ordthmeolem 23754 prdsxmetlem 24323 prdsbl 24449 iblcnlem1 25766 ellimc2 25855 rlimcnp 26947 xrlimcnp 26950 ftalem3 27057 dchreq 27241 2sqlem10 27411 dchrisum0flb 27493 pntpbnd1 27569 addsuniflem 27969 mulsuniflem 28104 wlkp1lem8 29571 pthdlem1 29657 crctcshwlkn0lem7 29704 wwlksnext 29781 clwwlkccatlem 29876 clwwlkel 29933 clwwlkwwlksb 29941 wwlksext2clwwlk 29944 clwwlknonex2lem2 29995 3wlkdlem4 30049 3pthdlem1 30051 upgr4cycl4dv4e 30072 dfconngr1 30075 cntzun 32869 ordtrest2NEW 33657 subfacp1lem3 34925 subfacp1lem5 34927 erdszelem8 34941 hfext 35912 bj-raldifsn 36712 finixpnum 37211 lindsadd 37219 lindsenlbs 37221 poimirlem26 37252 poimirlem27 37253 poimirlem32 37258 prdsbnd 37399 rrnequiv 37441 hdmap14lem13 41485 |
Copyright terms: Public domain | W3C validator |