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

Theorem ralunb 3528
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 3488 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
21imbi1i 316 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  ->  ph )  <->  ( ( x  e.  A  \/  x  e.  B )  ->  ph )
)
3 jaob 759 . . . . 5  |-  ( ( ( x  e.  A  \/  x  e.  B
)  ->  ph )  <->  ( (
x  e.  A  ->  ph )  /\  (
x  e.  B  ->  ph ) ) )
42, 3bitri 241 . . . 4  |-  ( ( x  e.  ( A  u.  B )  ->  ph )  <->  ( ( x  e.  A  ->  ph )  /\  ( x  e.  B  ->  ph ) ) )
54albii 1575 . . 3  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  ph )  <->  A. x
( ( x  e.  A  ->  ph )  /\  ( x  e.  B  ->  ph ) ) )
6 19.26 1603 . . 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 241 . 2  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  ph )  <->  ( A. x ( x  e.  A  ->  ph )  /\  A. x ( x  e.  B  ->  ph ) ) )
8 df-ral 2710 . 2  |-  ( A. x  e.  ( A  u.  B ) ph  <->  A. x
( x  e.  ( A  u.  B )  ->  ph ) )
9 df-ral 2710 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
10 df-ral 2710 . . 3  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
119, 10anbi12i 679 . 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 269 1  |-  ( A. x  e.  ( A  u.  B ) ph  <->  ( A. x  e.  A  ph  /\  A. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359   A.wal 1549    e. wcel 1725   A.wral 2705    u. cun 3318
This theorem is referenced by:  ralun  3529  ralprg  3857  raltpg  3859  ralunsn  4003  disjxun  4210  undifixp  7098  ixpfi2  7405  dffi3  7436  cantnfrescl  7632  fseqenlem1  7905  hashf1lem1  11704  rexfiuz  12151  prmind2  13090  prmreclem2  13285  lubun  14550  efgsp1  15369  unocv  16907  basdif0  17018  isclo  17151  ordtrest2  17268  ptbasfi  17613  ptcnplem  17653  ptrescn  17671  ordthmeolem  17833  prdsxmetlem  18398  prdsbl  18521  iblcnlem1  19679  ellimc2  19764  rlimcnp  20804  xrlimcnp  20807  ftalem3  20857  dchreq  21042  2sqlem10  21158  dchrisum0flb  21204  pntpbnd1  21280  4cycl4v4e  21653  4cycl4dv4e  21655  dfconngra1  21658  subfacp1lem3  24868  subfacp1lem5  24870  erdszelem8  24884  hfext  26124  prdsbnd  26502  rrnequiv  26544  cshwssizelem1  28280  lubunNEW  29771  hdmap14lem13  32681
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-v 2958  df-un 3325
  Copyright terms: Public domain W3C validator