Theorem ralunb 4150

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 4137	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1872	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 275	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3053	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3053	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 629	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 303	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3052   ∪ cun 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3443  df-un 3907

This theorem is referenced by:  ralun  4151  raldifeq  4447  ralprgf  4652  ralprg  4654  raltpg  4656  ralunsn  4851  disjxun  5097  naddunif  8623  undifixp  8876  ixpfi2  9254  dffi3  9338  fseqenlem1  9938  hashf1lem1  14382  pfxsuffeqwrdeq  14625  rexfiuz  15275  modfsummods  15720  modfsummod  15721  coprmproddvdslem  16593  prmind2  16616  prmreclem2  16849  lubun  18442  efgsp1  19670  unocv  21639  coe1fzgsumdlem  22251  evl1gsumdlem  22304  basdif0  22901  isclo  23035  ordtrest2  23152  ptbasfi  23529  ptcnplem  23569  ptrescn  23587  ordthmeolem  23749  prdsxmetlem  24316  prdsbl  24439  iblcnlem1  25749  ellimc2  25838  rlimcnp  26935  xrlimcnp  26938  ftalem3  27045  dchreq  27229  2sqlem10  27399  dchrisum0flb  27481  pntpbnd1  27557  addsuniflem  28001  mulsuniflem  28149  pw2cut2  28462  elreno2  28495  wlkp1lem8  29756  pthdlem1  29843  crctcshwlkn0lem7  29893  wwlksnext  29970  clwwlkccatlem  30068  clwwlkel  30125  clwwlkwwlksb  30133  wwlksext2clwwlk  30136  clwwlknonex2lem2  30187  3wlkdlem4  30241  3pthdlem1  30243  upgr4cycl4dv4e  30264  dfconngr1  30267  cntzun  33163  ordtrest2NEW  34082  subfacp1lem3  35378  subfacp1lem5  35380  erdszelem8  35394  hfext  36379  bj-raldifsn  37307  finixpnum  37808  lindsadd  37816  lindsenlbs  37818  poimirlem26  37849  poimirlem27  37850  poimirlem32  37855  prdsbnd  37996  rrnequiv  38038  hdmap14lem13  42208  usgrexmpl1lem  48334  usgrexmpl2lem  48339  usgrexmpl2trifr  48350