Theorem ralunb 4121

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 4108	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1823	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1874	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 274	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3068	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3068	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 626	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 302	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   ∈ wcel 2108  ∀wral 3063   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-un 3888

This theorem is referenced by:  ralun  4122  raldifeq  4421  ralprgf  4625  ralprg  4627  raltpg  4631  ralunsn  4822  disjxun  5068  undifixp  8680  ixpfi2  9047  dffi3  9120  fseqenlem1  9711  hashf1lem1  14096  hashf1lem1OLD  14097  pfxsuffeqwrdeq  14339  rexfiuz  14987  modfsummods  15433  modfsummod  15434  coprmproddvdslem  16295  prmind2  16318  prmreclem2  16546  lubun  18148  efgsp1  19258  unocv  20797  coe1fzgsumdlem  21382  evl1gsumdlem  21432  basdif0  22011  isclo  22146  ordtrest2  22263  ptbasfi  22640  ptcnplem  22680  ptrescn  22698  ordthmeolem  22860  prdsxmetlem  23429  prdsbl  23553  iblcnlem1  24857  ellimc2  24946  rlimcnp  26020  xrlimcnp  26023  ftalem3  26129  dchreq  26311  2sqlem10  26481  dchrisum0flb  26563  pntpbnd1  26639  wlkp1lem8  27950  pthdlem1  28035  crctcshwlkn0lem7  28082  wwlksnext  28159  clwwlkccatlem  28254  clwwlkel  28311  clwwlkwwlksb  28319  wwlksext2clwwlk  28322  clwwlknonex2lem2  28373  3wlkdlem4  28427  3pthdlem1  28429  upgr4cycl4dv4e  28450  dfconngr1  28453  cntzun  31222  ordtrest2NEW  31775  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem8  33060  hfext  34412  bj-raldifsn  35198  finixpnum  35689  lindsadd  35697  lindsenlbs  35699  poimirlem26  35730  poimirlem27  35731  poimirlem32  35736  prdsbnd  35878  rrnequiv  35920  hdmap14lem13  39821