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

Theorem ralunb 4017
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 3976 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
21imbi1i 341 . . . . 5 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝑥𝐵) → 𝜑))
3 jaob 947 . . . . 5 (((𝑥𝐴𝑥𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
42, 3bitri 267 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
54albii 1863 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
6 19.26 1916 . . 3 (∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
75, 6bitri 267 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
8 df-ral 3095 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑))
9 df-ral 3095 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
10 df-ral 3095 . . 3 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
119, 10anbi12i 620 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
127, 8, 113bitr4i 295 1 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  wo 836  wal 1599  wcel 2107  wral 3090  cun 3790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-v 3400  df-un 3797
This theorem is referenced by:  ralun  4018  raldifeq  4282  ralprgf  4461  raltpg  4465  ralunsn  4657  disjxun  4884  undifixp  8230  ixpfi2  8552  dffi3  8625  fseqenlem1  9180  hashf1lem1  13553  2swrdeqwrdeqOLD  13773  pfxsuffeqwrdeq  13807  rexfiuz  14494  modfsummods  14929  modfsummod  14930  coprmproddvdslem  15781  prmind2  15803  prmreclem2  16025  lubun  17509  efgsp1  18534  coe1fzgsumdlem  20067  evl1gsumdlem  20116  unocv  20423  basdif0  21165  isclo  21299  ordtrest2  21416  ptbasfi  21793  ptcnplem  21833  ptrescn  21851  ordthmeolem  22013  prdsxmetlem  22581  prdsbl  22704  iblcnlem1  23991  ellimc2  24078  rlimcnp  25144  xrlimcnp  25147  ftalem3  25253  dchreq  25435  2sqlem10  25605  dchrisum0flb  25651  pntpbnd1  25727  wlkp1lem8  27031  pthdlem1  27118  crctcshwlkn0lem7  27165  wwlksnext  27254  clwwlkccatlem  27369  clwwlkel  27437  clwwlkwwlksb  27451  wwlksext2clwwlk  27454  clwwlknonex2lem2  27510  3wlkdlem4  27565  3pthdlem1  27567  upgr4cycl4dv4e  27588  dfconngr1  27591  ordtrest2NEW  30567  subfacp1lem3  31763  subfacp1lem5  31765  erdszelem8  31779  ssltun1  32504  ssltun2  32505  hfext  32879  bj-raldifsn  33627  finixpnum  34019  lindsadd  34028  lindsenlbs  34030  poimirlem26  34061  poimirlem27  34062  poimirlem32  34067  prdsbnd  34216  rrnequiv  34258  hdmap14lem13  38034
  Copyright terms: Public domain W3C validator