Theorem ralunb 4017

Description: Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
ralunb	⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Proof of Theorem 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 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

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