Theorem ralunb 4118

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   ∈ wcel 2111  ∀wral 3106   ∪ cun 3879

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-un 3886

This theorem is referenced by:  ralun  4119  raldifeq  4397  ralprgf  4590  raltpg  4594  ralunsn  4786  disjxun  5028  undifixp  8481  ixpfi2  8806  dffi3  8879  fseqenlem1  9435  hashf1lem1  13809  pfxsuffeqwrdeq  14051  rexfiuz  14699  modfsummods  15140  modfsummod  15141  coprmproddvdslem  15996  prmind2  16019  prmreclem2  16243  lubun  17725  efgsp1  18855  unocv  20369  coe1fzgsumdlem  20930  evl1gsumdlem  20980  basdif0  21558  isclo  21692  ordtrest2  21809  ptbasfi  22186  ptcnplem  22226  ptrescn  22244  ordthmeolem  22406  prdsxmetlem  22975  prdsbl  23098  iblcnlem1  24391  ellimc2  24480  rlimcnp  25551  xrlimcnp  25554  ftalem3  25660  dchreq  25842  2sqlem10  26012  dchrisum0flb  26094  pntpbnd1  26170  wlkp1lem8  27470  pthdlem1  27555  crctcshwlkn0lem7  27602  wwlksnext  27679  clwwlkccatlem  27774  clwwlkel  27831  clwwlkwwlksb  27839  wwlksext2clwwlk  27842  clwwlknonex2lem2  27893  3wlkdlem4  27947  3pthdlem1  27949  upgr4cycl4dv4e  27970  dfconngr1  27973  cntzun  30745  ordtrest2NEW  31276  subfacp1lem3  32542  subfacp1lem5  32544  erdszelem8  32558  ssltun1  33382  ssltun2  33383  hfext  33757  bj-raldifsn  34515  finixpnum  35042  lindsadd  35050  lindsenlbs  35052  poimirlem26  35083  poimirlem27  35084  poimirlem32  35089  prdsbnd  35231  rrnequiv  35273  hdmap14lem13  39176