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

Theorem ralunb 3929
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 elun 3888 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
21imbi1i 338 . . . . 5 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝑥𝐵) → 𝜑))
3 jaob 857 . . . . 5 (((𝑥𝐴𝑥𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
42, 3bitri 264 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
54albii 1888 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
6 19.26 1939 . . 3 (∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
75, 6bitri 264 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
8 df-ral 3047 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑))
9 df-ral 3047 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
10 df-ral 3047 . . 3 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
119, 10anbi12i 735 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
127, 8, 113bitr4i 292 1 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  wal 1622  wcel 2131  wral 3042  cun 3705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-v 3334  df-un 3712
This theorem is referenced by:  ralun  3930  raldifeq  4195  ralprg  4370  raltpg  4372  ralunsn  4566  disjxun  4794  undifixp  8102  ixpfi2  8421  dffi3  8494  fseqenlem1  9029  hashf1lem1  13423  2swrdeqwrdeq  13645  rexfiuz  14278  modfsummods  14716  modfsummod  14717  coprmproddvdslem  15570  prmind2  15592  prmreclem2  15815  lubun  17316  efgsp1  18342  coe1fzgsumdlem  19865  evl1gsumdlem  19914  unocv  20218  basdif0  20951  isclo  21085  ordtrest2  21202  ptbasfi  21578  ptcnplem  21618  ptrescn  21636  ordthmeolem  21798  prdsxmetlem  22366  prdsbl  22489  iblcnlem1  23745  ellimc2  23832  rlimcnp  24883  xrlimcnp  24886  ftalem3  24992  dchreq  25174  2sqlem10  25344  dchrisum0flb  25390  pntpbnd1  25466  wlkp1lem8  26779  pthdlem1  26864  crctcshwlkn0lem7  26911  wwlksnext  27003  clwwlkccatlem  27104  clwwlkel  27167  clwwlkwwlksb  27176  wwlksext2clwwlk  27179  wwlksext2clwwlkOLD  27180  clwwlknonex2lem2  27249  3wlkdlem4  27306  3pthdlem1  27308  upgr4cycl4dv4e  27329  dfconngr1  27332  ordtrest2NEW  30270  subfacp1lem3  31463  subfacp1lem5  31465  erdszelem8  31479  ssltun1  32213  ssltun2  32214  hfext  32588  bj-raldifsn  33352  finixpnum  33699  lindsenlbs  33709  poimirlem26  33740  poimirlem27  33741  poimirlem32  33746  prdsbnd  33897  rrnequiv  33939  hdmap14lem13  37666  pfxsuffeqwrdeq  41908
  Copyright terms: Public domain W3C validator