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

Theorem ralunb 3624
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 3584 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
21imbi1i 323 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  ->  ph )  <->  ( ( x  e.  A  \/  x  e.  B )  ->  ph )
)
3 jaob 784 . . . . 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 1661 . . 3  |-  ( A. x ( x  e.  ( A  u.  B
)  ->  ph )  <->  A. x
( ( x  e.  A  ->  ph )  /\  ( x  e.  B  ->  ph ) ) )
6 19.26 1701 . . 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 2759 . 2  |-  ( A. x  e.  ( A  u.  B ) ph  <->  A. x
( x  e.  ( A  u.  B )  ->  ph ) )
9 df-ral 2759 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
10 df-ral 2759 . . 3  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
119, 10anbi12i 695 . 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 366    /\ wa 367   A.wal 1403    e. wcel 1842   A.wral 2754    u. cun 3412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-v 3061  df-un 3419
This theorem is referenced by:  ralun  3625  raldifeq  3861  ralprg  4021  raltpg  4023  ralunsn  4179  disjxun  4393  undifixp  7543  ixpfi2  7852  dffi3  7925  fseqenlem1  8437  hashf1lem1  12553  2swrdeqwrdeq  12734  rexfiuz  13329  modfsummods  13758  modfsummod  13759  prmind2  14437  prmreclem2  14644  lubun  16077  efgsp1  17079  coe1fzgsumdlem  18663  evl1gsumdlem  18712  unocv  19009  basdif0  19746  isclo  19881  ordtrest2  19998  ptbasfi  20374  ptcnplem  20414  ptrescn  20432  ordthmeolem  20594  prdsxmetlem  21163  prdsbl  21286  iblcnlem1  22486  ellimc2  22573  rlimcnp  23621  xrlimcnp  23624  ftalem3  23729  dchreq  23914  2sqlem10  24030  dchrisum0flb  24076  pntpbnd1  24152  4cycl4v4e  25083  4cycl4dv4e  25085  dfconngra1  25088  wwlknext  25141  clwwlkel  25210  wwlkext2clwwlk  25220  numclwwlkovf2ex  25503  ordtrest2NEW  28358  subfacp1lem3  29479  subfacp1lem5  29481  erdszelem8  29495  hfext  30521  finixpnum  31410  prdsbnd  31571  rrnequiv  31613  hdmap14lem13  34903  pfxsuffeqwrdeq  37893
  Copyright terms: Public domain W3C validator