Theorem ralunb 4220

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   ∈ wcel 2108  ∀wral 3067   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-un 3981

This theorem is referenced by:  ralun  4221  raldifeq  4517  ralprgf  4717  ralprg  4719  raltpg  4723  ralunsn  4918  disjxun  5164  naddunif  8749  undifixp  8992  ixpfi2  9420  dffi3  9500  fseqenlem1  10093  hashf1lem1  14504  pfxsuffeqwrdeq  14746  rexfiuz  15396  modfsummods  15841  modfsummod  15842  coprmproddvdslem  16709  prmind2  16732  prmreclem2  16964  lubun  18585  efgsp1  19779  unocv  21721  coe1fzgsumdlem  22328  evl1gsumdlem  22381  basdif0  22981  isclo  23116  ordtrest2  23233  ptbasfi  23610  ptcnplem  23650  ptrescn  23668  ordthmeolem  23830  prdsxmetlem  24399  prdsbl  24525  iblcnlem1  25843  ellimc2  25932  rlimcnp  27026  xrlimcnp  27029  ftalem3  27136  dchreq  27320  2sqlem10  27490  dchrisum0flb  27572  pntpbnd1  27648  addsuniflem  28052  mulsuniflem  28193  wlkp1lem8  29716  pthdlem1  29802  crctcshwlkn0lem7  29849  wwlksnext  29926  clwwlkccatlem  30021  clwwlkel  30078  clwwlkwwlksb  30086  wwlksext2clwwlk  30089  clwwlknonex2lem2  30140  3wlkdlem4  30194  3pthdlem1  30196  upgr4cycl4dv4e  30217  dfconngr1  30220  cntzun  33044  ordtrest2NEW  33869  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem8  35166  hfext  36147  bj-raldifsn  37066  finixpnum  37565  lindsadd  37573  lindsenlbs  37575  poimirlem26  37606  poimirlem27  37607  poimirlem32  37612  prdsbnd  37753  rrnequiv  37795  hdmap14lem13  41837  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2trifr  47852