Theorem ralunb 4125

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		elunant 4112	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1822	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1873	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 274	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3069	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3069	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3069	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 627	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 303	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   ∈ wcel 2106  ∀wral 3064   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-un 3892

This theorem is referenced by:  ralun  4126  raldifeq  4424  ralprgf  4628  ralprg  4630  raltpg  4634  ralunsn  4825  disjxun  5072  undifixp  8722  ixpfi2  9117  dffi3  9190  fseqenlem1  9780  hashf1lem1  14168  hashf1lem1OLD  14169  pfxsuffeqwrdeq  14411  rexfiuz  15059  modfsummods  15505  modfsummod  15506  coprmproddvdslem  16367  prmind2  16390  prmreclem2  16618  lubun  18233  efgsp1  19343  unocv  20885  coe1fzgsumdlem  21472  evl1gsumdlem  21522  basdif0  22103  isclo  22238  ordtrest2  22355  ptbasfi  22732  ptcnplem  22772  ptrescn  22790  ordthmeolem  22952  prdsxmetlem  23521  prdsbl  23647  iblcnlem1  24952  ellimc2  25041  rlimcnp  26115  xrlimcnp  26118  ftalem3  26224  dchreq  26406  2sqlem10  26576  dchrisum0flb  26658  pntpbnd1  26734  wlkp1lem8  28048  pthdlem1  28134  crctcshwlkn0lem7  28181  wwlksnext  28258  clwwlkccatlem  28353  clwwlkel  28410  clwwlkwwlksb  28418  wwlksext2clwwlk  28421  clwwlknonex2lem2  28472  3wlkdlem4  28526  3pthdlem1  28528  upgr4cycl4dv4e  28549  dfconngr1  28552  cntzun  31320  ordtrest2NEW  31873  subfacp1lem3  33144  subfacp1lem5  33146  erdszelem8  33160  hfext  34485  bj-raldifsn  35271  finixpnum  35762  lindsadd  35770  lindsenlbs  35772  poimirlem26  35803  poimirlem27  35804  poimirlem32  35809  prdsbnd  35951  rrnequiv  35993  hdmap14lem13  39894