Theorem ralunb 4151

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1560   ∈ wcel 2144  ∀wral 3078   ∪ cun 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-v 3458  df-un 3911

This theorem is referenced by:  ralun  4152  raldifeq  4449  ralprgf  4655  ralprg  4657  raltpg  4659  ralunsn  4854  disjxun  5100  naddunif  8666  undifixp  8918  ixpfi2  9295  dffi3  9379  fseqenlem1  9982  hashf1lem1  14470  pfxsuffeqwrdeq  14713  rexfiuz  15377  modfsummods  15823  modfsummod  15824  coprmproddvdslem  16698  prmind2  16721  prmreclem2  16955  lubun  18549  efgsp1  19779  unocv  21734  coe1fzgsumdlem  22368  evl1gsumdlem  22421  basdif0  23015  isclo  23149  ordtrest2  23266  ptbasfi  23643  ptcnplem  23683  ptrescn  23701  ordthmeolem  23863  prdsxmetlem  24430  prdsbl  24553  iblcnlem1  25852  ellimc2  25941  rlimcnp  27032  xrlimcnp  27035  ftalem3  27141  dchreq  27324  2sqlem10  27494  dchrisum0flb  27576  pntpbnd1  27652  addsuniflem  28096  mulsuniflem  28244  pw2cut2  28557  elreno2  28590  wlkp1lem8  29881  pthdlem1  29968  crctcshwlkn0lem7  30018  wwlksnext  30095  clwwlkccatlem  30193  clwwlkel  30250  clwwlkwwlksb  30258  wwlksext2clwwlk  30261  clwwlknonex2lem2  30312  3wlkdlem4  30366  3pthdlem1  30368  upgr4cycl4dv4e  30389  dfconngr1  30392  cntzun  33261  ordtrest2NEW  34222  subfacp1lem3  35537  subfacp1lem5  35539  erdszelem8  35553  hfext  36538  bj-raldifsn  37595  finixpnum  38109  lindsadd  38117  lindsenlbs  38119  poimirlem26  38150  poimirlem27  38151  poimirlem32  38156  prdsbnd  38297  rrnequiv  38339  hdmap14lem13  42509  usgrexmpl1lem  48648  usgrexmpl2lem  48653  usgrexmpl2trifr  48664