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

Theorem ralunb 3492
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 3452 . . . . . 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 1572 . . 3  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  ph )  <->  A. x
( ( x  e.  A  ->  ph )  /\  ( x  e.  B  ->  ph ) ) )
6 19.26 1600 . . 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 2675 . 2  |-  ( A. x  e.  ( A  u.  B ) ph  <->  A. x
( x  e.  ( A  u.  B )  ->  ph ) )
9 df-ral 2675 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
10 df-ral 2675 . . 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 1546    e. wcel 1721   A.wral 2670    u. cun 3282
This theorem is referenced by:  ralun  3493  ralprg  3821  raltpg  3823  ralunsn  3967  disjxun  4174  undifixp  7061  ixpfi2  7367  dffi3  7398  cantnfrescl  7592  fseqenlem1  7865  hashf1lem1  11663  rexfiuz  12110  prmind2  13049  prmreclem2  13244  lubun  14509  efgsp1  15328  unocv  16866  basdif0  16977  isclo  17110  ordtrest2  17226  ptbasfi  17570  ptcnplem  17610  ptrescn  17628  ordthmeolem  17790  prdsxmetlem  18355  prdsbl  18478  iblcnlem1  19636  ellimc2  19721  rlimcnp  20761  xrlimcnp  20764  ftalem3  20814  dchreq  20999  2sqlem10  21115  dchrisum0flb  21161  pntpbnd1  21237  4cycl4v4e  21610  4cycl4dv4e  21612  dfconngra1  21615  subfacp1lem3  24825  subfacp1lem5  24827  erdszelem8  24841  hfext  26032  prdsbnd  26396  rrnequiv  26438  lubunNEW  29460  hdmap14lem13  32370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ral 2675  df-v 2922  df-un 3289
  Copyright terms: Public domain W3C validator