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

Theorem ralunb 3952
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 3911 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
21imbi1i 339 . . . . 5 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝑥𝐵) → 𝜑))
3 jaob 973 . . . . 5 (((𝑥𝐴𝑥𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
42, 3bitri 265 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
54albii 1898 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
6 19.26 1952 . . 3 (∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
75, 6bitri 265 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
8 df-ral 3069 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑))
9 df-ral 3069 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
10 df-ral 3069 . . 3 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
119, 10anbi12i 613 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
127, 8, 113bitr4i 293 1 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 383  wo 863  wal 1632  wcel 2148  wral 3064  cun 3727
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ral 3069  df-v 3357  df-un 3734
This theorem is referenced by:  ralun  3953  raldifeq  4210  ralprg  4382  raltpg  4384  ralunsn  4571  disjxun  4795  undifixp  8119  ixpfi2  8441  dffi3  8514  fseqenlem1  9068  hashf1lem1  13463  2swrdeqwrdeq  13684  rexfiuz  14317  modfsummods  14754  modfsummod  14755  coprmproddvdslem  15604  prmind2  15626  prmreclem2  15848  lubun  17351  efgsp1  18377  coe1fzgsumdlem  19906  evl1gsumdlem  19955  unocv  20261  basdif0  20998  isclo  21132  ordtrest2  21249  ptbasfi  21625  ptcnplem  21665  ptrescn  21683  ordthmeolem  21845  prdsxmetlem  22413  prdsbl  22536  iblcnlem1  23795  ellimc2  23882  rlimcnp  24934  xrlimcnp  24937  ftalem3  25043  dchreq  25225  2sqlem10  25395  dchrisum0flb  25441  pntpbnd1  25517  wlkp1lem8  26833  pthdlem1  26918  crctcshwlkn0lem7  26965  wwlksnext  27058  clwwlkccatlem  27160  clwwlkel  27223  clwwlkwwlksb  27232  wwlksext2clwwlk  27235  wwlksext2clwwlkOLD  27236  clwwlknonex2lem2  27305  3wlkdlem4  27363  3pthdlem1  27365  upgr4cycl4dv4e  27386  dfconngr1  27389  ordtrest2NEW  30326  subfacp1lem3  31519  subfacp1lem5  31521  erdszelem8  31535  ssltun1  32269  ssltun2  32270  hfext  32644  bj-raldifsn  33403  finixpnum  33744  lindsenlbs  33754  poimirlem26  33785  poimirlem27  33786  poimirlem32  33791  prdsbnd  33940  rrnequiv  33982  hdmap14lem13  37705  pfxsuffeqwrdeq  41958
  Copyright terms: Public domain W3C validator