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

Theorem ralunb 3684
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 3644 . . . . . 6
21imbi1i 325 . . . . 5
3 jaob 783 . . . . 5
42, 3bitri 249 . . . 4
54albii 1640 . . 3
6 19.26 1680 . . 3
75, 6bitri 249 . 2
8 df-ral 2812 . 2
9 df-ral 2812 . . 3
10 df-ral 2812 . . 3
119, 10anbi12i 697 . 2
127, 8, 113bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  \/wo 368  /\wa 369  A.wal 1393  e.wcel 1818  A.wral 2807  u.cun 3473
This theorem is referenced by:  ralun  3685  raldifeq  3917  ralprg  4078  raltpg  4080  ralunsn  4237  disjxun  4450  undifixp  7525  ixpfi2  7838  dffi3  7911  fseqenlem1  8426  hashf1lem1  12504  wrdeqswrdlsw  12674  2swrdeqwrdeq  12678  rexfiuz  13180  modfsummods  13607  modfsummod  13608  prmind2  14228  prmreclem2  14435  lubun  15753  efgsp1  16755  coe1fzgsumdlem  18343  evl1gsumdlem  18392  unocv  18711  basdif0  19454  isclo  19588  ordtrest2  19705  ptbasfi  20082  ptcnplem  20122  ptrescn  20140  ordthmeolem  20302  prdsxmetlem  20871  prdsbl  20994  iblcnlem1  22194  ellimc2  22281  rlimcnp  23295  xrlimcnp  23298  ftalem3  23348  dchreq  23533  2sqlem10  23649  dchrisum0flb  23695  pntpbnd1  23771  4cycl4v4e  24666  4cycl4dv4e  24668  dfconngra1  24671  wwlknext  24724  clwwlkel  24793  wwlkext2clwwlk  24803  numclwwlkovf2ex  25086  ordtrest2NEW  27905  subfacp1lem3  28626  subfacp1lem5  28628  erdszelem8  28642  hfext  29840  finixpnum  30038  prdsbnd  30289  rrnequiv  30331  hdmap14lem13  37610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-un 3480
  Copyright terms: Public domain W3C validator