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

Theorem ralunb 3635
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 3595 . . . . . 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 1611 . . 3  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  ph )  <->  A. x
( ( x  e.  A  ->  ph )  /\  ( x  e.  B  ->  ph ) ) )
6 19.26 1648 . . 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 2800 . 2  |-  ( A. x  e.  ( A  u.  B ) ph  <->  A. x
( x  e.  ( A  u.  B )  ->  ph ) )
9 df-ral 2800 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
10 df-ral 2800 . . 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 1368    e. wcel 1758   A.wral 2795    u. cun 3424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-v 3070  df-un 3431
This theorem is referenced by:  ralun  3636  raldifeq  3866  ralprg  4023  raltpg  4025  ralunsn  4177  disjxun  4388  undifixp  7399  ixpfi2  7710  dffi3  7782  cantnfrescl  7985  fseqenlem1  8295  hashf1lem1  12310  wrdeqswrdlsw  12445  2swrdeqwrdeq  12449  rexfiuz  12937  prmind2  13876  prmreclem2  14080  lubun  15395  efgsp1  16338  evl1gsumdlem  17899  unocv  18214  basdif0  18674  isclo  18807  ordtrest2  18924  ptbasfi  19270  ptcnplem  19310  ptrescn  19328  ordthmeolem  19490  prdsxmetlem  20059  prdsbl  20182  iblcnlem1  21381  ellimc2  21468  rlimcnp  22475  xrlimcnp  22478  ftalem3  22528  dchreq  22713  2sqlem10  22829  dchrisum0flb  22875  pntpbnd1  22951  4cycl4v4e  23687  4cycl4dv4e  23689  dfconngra1  23692  ordtrest2NEW  26487  subfacp1lem3  27204  subfacp1lem5  27206  erdszelem8  27220  hfext  28355  finixpnum  28552  prdsbnd  28830  rrnequiv  28872  modfsummods  30382  modfsummod  30383  wwlknext  30494  clwwlkel  30593  wwlkext2clwwlk  30603  numclwwlkovf2ex  30817  coe1fzgsumdlem  30979  hdmap14lem13  35834
  Copyright terms: Public domain W3C validator