Theorem ralunb 4169

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 4156	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1871	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 277	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3145	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3145	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3145	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 628	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 305	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   ∈ wcel 2114  ∀wral 3140   ∪ cun 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-v 3498  df-un 3943

This theorem is referenced by:  ralun  4170  raldifeq  4441  ralprgf  4632  raltpg  4636  ralunsn  4826  disjxun  5066  undifixp  8500  ixpfi2  8824  dffi3  8897  fseqenlem1  9452  hashf1lem1  13816  pfxsuffeqwrdeq  14062  rexfiuz  14709  modfsummods  15150  modfsummod  15151  coprmproddvdslem  16008  prmind2  16031  prmreclem2  16255  lubun  17735  efgsp1  18865  coe1fzgsumdlem  20471  evl1gsumdlem  20521  unocv  20826  basdif0  21563  isclo  21697  ordtrest2  21814  ptbasfi  22191  ptcnplem  22231  ptrescn  22249  ordthmeolem  22411  prdsxmetlem  22980  prdsbl  23103  iblcnlem1  24390  ellimc2  24477  rlimcnp  25545  xrlimcnp  25548  ftalem3  25654  dchreq  25836  2sqlem10  26006  dchrisum0flb  26088  pntpbnd1  26164  wlkp1lem8  27464  pthdlem1  27549  crctcshwlkn0lem7  27596  wwlksnext  27673  clwwlkccatlem  27769  clwwlkel  27827  clwwlkwwlksb  27835  wwlksext2clwwlk  27838  clwwlknonex2lem2  27889  3wlkdlem4  27943  3pthdlem1  27945  upgr4cycl4dv4e  27966  dfconngr1  27969  cntzun  30697  ordtrest2NEW  31168  subfacp1lem3  32431  subfacp1lem5  32433  erdszelem8  32447  ssltun1  33271  ssltun2  33272  hfext  33646  bj-raldifsn  34394  finixpnum  34879  lindsadd  34887  lindsenlbs  34889  poimirlem26  34920  poimirlem27  34921  poimirlem32  34926  prdsbnd  35073  rrnequiv  35115  hdmap14lem13  39018