Theorem ralunb 3756

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 3715	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2	1	imbi1i 338	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → 𝜑))
3		jaob 818	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 263	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
5	4	albii 1737	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
6		19.26 1786	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
7	5, 6	bitri 263	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
8		df-ral 2901	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
9		df-ral 2901	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
10		df-ral 2901	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
11	9, 10	anbi12i 729	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
12	7, 8, 11	3bitr4i 291	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383  ∀wal 1473   ∈ wcel 1977  ∀wral 2896   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-un 3545

This theorem is referenced by:  ralun  3757  raldifeq  4011  ralprg  4181  raltpg  4183  ralunsn  4360  disjxun  4581  undifixp  7830  ixpfi2  8147  dffi3  8220  fseqenlem1  8730  hashf1lem1  13096  2swrdeqwrdeq  13305  rexfiuz  13935  modfsummods  14366  modfsummod  14367  coprmproddvdslem  15214  prmind2  15236  prmreclem2  15459  lubun  16946  efgsp1  17973  coe1fzgsumdlem  19492  evl1gsumdlem  19541  unocv  19843  basdif0  20568  isclo  20701  ordtrest2  20818  ptbasfi  21194  ptcnplem  21234  ptrescn  21252  ordthmeolem  21414  prdsxmetlem  21983  prdsbl  22106  iblcnlem1  23360  ellimc2  23447  rlimcnp  24492  xrlimcnp  24495  ftalem3  24601  dchreq  24783  2sqlem10  24953  dchrisum0flb  24999  pntpbnd1  25075  4cycl4v4e  26194  4cycl4dv4e  26196  dfconngra1  26199  wwlknext  26252  clwwlkel  26321  wwlkext2clwwlk  26331  numclwwlkovf2ex  26613  ordtrest2NEW  29297  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem8  30434  hfext  31460  finixpnum  32564  lindsenlbs  32574  poimirlem26  32605  poimirlem27  32606  poimirlem32  32611  prdsbnd  32762  rrnequiv  32804  hdmap14lem13  36190  pfxsuffeqwrdeq  40269  1wlkp1lem8  40889  pthdlem1  40972  crctcsh1wlkn0lem7  41019  wwlksnext  41099  clwwlksel  41221  wwlksext2clwwlk  41231  31wlkdlem4  41329  3pthdlem1  41331  upgr4cycl4dv4e  41352  dfconngr1  41355  av-numclwwlkovf2ex  41517