Theorem ralunb 4192

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   ∈ wcel 2107  ∀wral 3062   ∪ cun 3947

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-un 3954

This theorem is referenced by:  ralun  4193  raldifeq  4494  ralprgf  4697  ralprg  4699  raltpg  4703  ralunsn  4895  disjxun  5147  naddunif  8692  undifixp  8928  ixpfi2  9350  dffi3  9426  fseqenlem1  10019  hashf1lem1  14415  hashf1lem1OLD  14416  pfxsuffeqwrdeq  14648  rexfiuz  15294  modfsummods  15739  modfsummod  15740  coprmproddvdslem  16599  prmind2  16622  prmreclem2  16850  lubun  18468  efgsp1  19605  unocv  21233  coe1fzgsumdlem  21825  evl1gsumdlem  21875  basdif0  22456  isclo  22591  ordtrest2  22708  ptbasfi  23085  ptcnplem  23125  ptrescn  23143  ordthmeolem  23305  prdsxmetlem  23874  prdsbl  24000  iblcnlem1  25305  ellimc2  25394  rlimcnp  26470  xrlimcnp  26473  ftalem3  26579  dchreq  26761  2sqlem10  26931  dchrisum0flb  27013  pntpbnd1  27089  addsuniflem  27487  mulsuniflem  27607  wlkp1lem8  28968  pthdlem1  29054  crctcshwlkn0lem7  29101  wwlksnext  29178  clwwlkccatlem  29273  clwwlkel  29330  clwwlkwwlksb  29338  wwlksext2clwwlk  29341  clwwlknonex2lem2  29392  3wlkdlem4  29446  3pthdlem1  29448  upgr4cycl4dv4e  29469  dfconngr1  29472  cntzun  32243  ordtrest2NEW  32934  subfacp1lem3  34204  subfacp1lem5  34206  erdszelem8  34220  hfext  35186  bj-raldifsn  36029  finixpnum  36521  lindsadd  36529  lindsenlbs  36531  poimirlem26  36562  poimirlem27  36563  poimirlem32  36568  prdsbnd  36709  rrnequiv  36751  hdmap14lem13  40799