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

Theorem ralunb 3680
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  |-  ( A. x  e.  ( A  u.  B ) ph  <->  ( A. x  e.  A  ph  /\  A. x  e.  B  ph ) )

Proof of Theorem ralunb
StepHypRef Expression
1 elun 3640 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
21imbi1i 325 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  ->  ph )  <->  ( ( x  e.  A  \/  x  e.  B )  ->  ph )
)
3 jaob 781 . . . . 5  |-  ( ( ( x  e.  A  \/  x  e.  B
)  ->  ph )  <->  ( (
x  e.  A  ->  ph )  /\  (
x  e.  B  ->  ph ) ) )
42, 3bitri 249 . . . 4  |-  ( ( x  e.  ( A  u.  B )  ->  ph )  <->  ( ( x  e.  A  ->  ph )  /\  ( x  e.  B  ->  ph ) ) )
54albii 1615 . . 3  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  ph )  <->  A. x
( ( x  e.  A  ->  ph )  /\  ( x  e.  B  ->  ph ) ) )
6 19.26 1652 . . 3  |-  ( A. x ( ( x  e.  A  ->  ph )  /\  ( x  e.  B  ->  ph ) )  <->  ( A. x ( x  e.  A  ->  ph )  /\  A. x ( x  e.  B  ->  ph ) ) )
75, 6bitri 249 . 2  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  ph )  <->  ( A. x ( x  e.  A  ->  ph )  /\  A. x ( x  e.  B  ->  ph ) ) )
8 df-ral 2814 . 2  |-  ( A. x  e.  ( A  u.  B ) ph  <->  A. x
( x  e.  ( A  u.  B )  ->  ph ) )
9 df-ral 2814 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
10 df-ral 2814 . . 3  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
119, 10anbi12i 697 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  B  ph )  <->  ( A. x
( x  e.  A  ->  ph )  /\  A. x ( x  e.  B  ->  ph ) ) )
127, 8, 113bitr4i 277 1  |-  ( A. x  e.  ( A  u.  B ) ph  <->  ( A. x  e.  A  ph  /\  A. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369   A.wal 1372    e. wcel 1762   A.wral 2809    u. cun 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ral 2814  df-v 3110  df-un 3476
This theorem is referenced by:  ralun  3681  raldifeq  3911  ralprg  4071  raltpg  4073  ralunsn  4228  disjxun  4440  undifixp  7497  ixpfi2  7809  dffi3  7882  cantnfrescl  8086  fseqenlem1  8396  hashf1lem1  12459  wrdeqswrdlsw  12626  2swrdeqwrdeq  12630  rexfiuz  13131  modfsummods  13558  modfsummod  13559  prmind2  14078  prmreclem2  14285  lubun  15601  efgsp1  16546  coe1fzgsumdlem  18109  evl1gsumdlem  18158  unocv  18473  basdif0  19216  isclo  19349  ordtrest2  19466  ptbasfi  19812  ptcnplem  19852  ptrescn  19870  ordthmeolem  20032  prdsxmetlem  20601  prdsbl  20724  iblcnlem1  21924  ellimc2  22011  rlimcnp  23018  xrlimcnp  23021  ftalem3  23071  dchreq  23256  2sqlem10  23372  dchrisum0flb  23418  pntpbnd1  23494  4cycl4v4e  24330  4cycl4dv4e  24332  dfconngra1  24335  wwlknext  24388  clwwlkel  24457  wwlkext2clwwlk  24467  numclwwlkovf2ex  24751  ordtrest2NEW  27529  subfacp1lem3  28254  subfacp1lem5  28256  erdszelem8  28270  hfext  29405  finixpnum  29603  prdsbnd  29881  rrnequiv  29923  hdmap14lem13  36557
  Copyright terms: Public domain W3C validator