![]() |
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 | elun 3976 | . . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
2 | 1 | imbi1i 341 | . . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → 𝜑)) |
3 | jaob 947 | . . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑))) | |
4 | 2, 3 | bitri 267 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑))) |
5 | 4 | albii 1863 | . . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑))) |
6 | 19.26 1916 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))) | |
7 | 5, 6 | bitri 267 | . 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))) |
8 | df-ral 3095 | . 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑)) | |
9 | df-ral 3095 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
10 | df-ral 3095 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) | |
11 | 9, 10 | anbi12i 620 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))) |
12 | 7, 8, 11 | 3bitr4i 295 | 1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∨ wo 836 ∀wal 1599 ∈ wcel 2107 ∀wral 3090 ∪ cun 3790 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-v 3400 df-un 3797 |
This theorem is referenced by: ralun 4018 raldifeq 4282 ralprgf 4461 raltpg 4465 ralunsn 4657 disjxun 4884 undifixp 8230 ixpfi2 8552 dffi3 8625 fseqenlem1 9180 hashf1lem1 13553 2swrdeqwrdeqOLD 13773 pfxsuffeqwrdeq 13807 rexfiuz 14494 modfsummods 14929 modfsummod 14930 coprmproddvdslem 15781 prmind2 15803 prmreclem2 16025 lubun 17509 efgsp1 18534 coe1fzgsumdlem 20067 evl1gsumdlem 20116 unocv 20423 basdif0 21165 isclo 21299 ordtrest2 21416 ptbasfi 21793 ptcnplem 21833 ptrescn 21851 ordthmeolem 22013 prdsxmetlem 22581 prdsbl 22704 iblcnlem1 23991 ellimc2 24078 rlimcnp 25144 xrlimcnp 25147 ftalem3 25253 dchreq 25435 2sqlem10 25605 dchrisum0flb 25651 pntpbnd1 25727 wlkp1lem8 27031 pthdlem1 27118 crctcshwlkn0lem7 27165 wwlksnext 27254 clwwlkccatlem 27369 clwwlkel 27437 clwwlkwwlksb 27451 wwlksext2clwwlk 27454 clwwlknonex2lem2 27510 3wlkdlem4 27565 3pthdlem1 27567 upgr4cycl4dv4e 27588 dfconngr1 27591 ordtrest2NEW 30567 subfacp1lem3 31763 subfacp1lem5 31765 erdszelem8 31779 ssltun1 32504 ssltun2 32505 hfext 32879 bj-raldifsn 33627 finixpnum 34019 lindsadd 34028 lindsenlbs 34030 poimirlem26 34061 poimirlem27 34062 poimirlem32 34067 prdsbnd 34216 rrnequiv 34258 hdmap14lem13 38034 |
Copyright terms: Public domain | W3C validator |