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

Theorem ralunb 3534
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 3494 . . . . . 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 776 . . . . 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 2718 . 2  |-  ( A. x  e.  ( A  u.  B ) ph  <->  A. x
( x  e.  ( A  u.  B )  ->  ph ) )
9 df-ral 2718 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
10 df-ral 2718 . . 3  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
119, 10anbi12i 692 . 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 1362    e. wcel 1761   A.wral 2713    u. cun 3323
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 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-v 2972  df-un 3330
This theorem is referenced by:  ralun  3535  raldifeq  3765  ralprg  3922  raltpg  3924  ralunsn  4076  disjxun  4287  undifixp  7295  ixpfi2  7605  dffi3  7677  cantnfrescl  7880  fseqenlem1  8190  hashf1lem1  12204  wrdeqswrdlsw  12339  2swrdeqwrdeq  12343  rexfiuz  12831  prmind2  13770  prmreclem2  13974  lubun  15289  efgsp1  16227  unocv  18064  basdif0  18517  isclo  18650  ordtrest2  18767  ptbasfi  19113  ptcnplem  19153  ptrescn  19171  ordthmeolem  19333  prdsxmetlem  19902  prdsbl  20025  iblcnlem1  21224  ellimc2  21311  rlimcnp  22318  xrlimcnp  22321  ftalem3  22371  dchreq  22556  2sqlem10  22672  dchrisum0flb  22718  pntpbnd1  22794  4cycl4v4e  23487  4cycl4dv4e  23489  dfconngra1  23492  ordtrest2NEW  26289  subfacp1lem3  27000  subfacp1lem5  27002  erdszelem8  27016  hfext  28150  finixpnum  28339  prdsbnd  28617  rrnequiv  28659  modfsummods  30169  modfsummod  30170  wwlknext  30281  clwwlkel  30380  wwlkext2clwwlk  30390  numclwwlkovf2ex  30604  hdmap14lem13  35250
  Copyright terms: Public domain W3C validator