MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralunb Structured version   Visualization version   GIF version

Theorem ralunb 4189
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
StepHypRef Expression
1 elunant 4176 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
21albii 1813 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
3 19.26 1865 . . 3 (∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
42, 3bitri 274 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
5 df-ral 3051 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑))
6 df-ral 3051 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
7 df-ral 3051 . . 3 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
86, 7anbi12i 626 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
94, 5, 83bitr4i 302 1 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1531  wcel 2098  wral 3050  cun 3942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-un 3949
This theorem is referenced by:  ralun  4190  raldifeq  4495  ralprgf  4698  ralprg  4700  raltpg  4704  ralunsn  4896  disjxun  5147  naddunif  8714  undifixp  8953  ixpfi2  9381  dffi3  9461  fseqenlem1  10054  hashf1lem1  14456  hashf1lem1OLD  14457  pfxsuffeqwrdeq  14689  rexfiuz  15335  modfsummods  15780  modfsummod  15781  coprmproddvdslem  16641  prmind2  16664  prmreclem2  16894  lubun  18515  efgsp1  19709  unocv  21634  coe1fzgsumdlem  22252  evl1gsumdlem  22305  basdif0  22905  isclo  23040  ordtrest2  23157  ptbasfi  23534  ptcnplem  23574  ptrescn  23592  ordthmeolem  23754  prdsxmetlem  24323  prdsbl  24449  iblcnlem1  25766  ellimc2  25855  rlimcnp  26947  xrlimcnp  26950  ftalem3  27057  dchreq  27241  2sqlem10  27411  dchrisum0flb  27493  pntpbnd1  27569  addsuniflem  27969  mulsuniflem  28104  wlkp1lem8  29571  pthdlem1  29657  crctcshwlkn0lem7  29704  wwlksnext  29781  clwwlkccatlem  29876  clwwlkel  29933  clwwlkwwlksb  29941  wwlksext2clwwlk  29944  clwwlknonex2lem2  29995  3wlkdlem4  30049  3pthdlem1  30051  upgr4cycl4dv4e  30072  dfconngr1  30075  cntzun  32869  ordtrest2NEW  33657  subfacp1lem3  34925  subfacp1lem5  34927  erdszelem8  34941  hfext  35912  bj-raldifsn  36712  finixpnum  37211  lindsadd  37219  lindsenlbs  37221  poimirlem26  37252  poimirlem27  37253  poimirlem32  37258  prdsbnd  37399  rrnequiv  37441  hdmap14lem13  41485
  Copyright terms: Public domain W3C validator