Theorem ralunb 3794

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

Step	Hyp	Ref	Expression
1		elun 3753	. . . . . 6 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
2	1	imbi1i 339	. . . . 5 |- ( ( x e. ( A u. B ) -> ph ) <-> ( ( x e. A \/ x e. B ) -> ph ) )
3		jaob 822	. . . . 5 |- ( ( ( x e. A \/ x e. B ) -> ph ) <-> ( ( x e. A -> ph ) /\ ( x e. B -> ph ) ) )
4	2, 3	bitri 264	. . . 4 |- ( ( x e. ( A u. B ) -> ph ) <-> ( ( x e. A -> ph ) /\ ( x e. B -> ph ) ) )
5	4	albii 1747	. . 3 |- ( A. x ( x e. ( A u. B ) -> ph ) <-> A. x ( ( x e. A -> ph ) /\ ( x e. B -> ph ) ) )
6		19.26 1798	. . 3 |- ( A. x ( ( x e. A -> ph ) /\ ( x e. B -> ph ) ) <-> ( A. x ( x e. A -> ph ) /\ A. x ( x e. B -> ph ) ) )
7	5, 6	bitri 264	. 2 |- ( A. x ( x e. ( A u. B ) -> ph ) <-> ( A. x ( x e. A -> ph ) /\ A. x ( x e. B -> ph ) ) )
8		df-ral 2917	. 2 |- ( A. x e. ( A u. B ) ph <-> A. x ( x e. ( A u. B ) -> ph ) )
9		df-ral 2917	. . 3 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
10		df-ral 2917	. . 3 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
11	9, 10	anbi12i 733	. 2 |- ( ( A. x e. A ph /\ A. x e. B ph ) <-> ( A. x ( x e. A -> ph ) /\ A. x ( x e. B -> ph ) ) )
12	7, 8, 11	3bitr4i 292	1 |- ( A. x e. ( A u. B ) ph <-> ( A. x e. A ph /\ A. x e. B ph ) )

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   A.wal 1481   e. wcel 1990   A.wral 2912   u. cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-un 3579

This theorem is referenced by:  ralun  3795  raldifeq  4059  ralprg  4234  raltpg  4236  ralunsn  4422  disjxun  4651  undifixp  7944  ixpfi2  8264  dffi3  8337  fseqenlem1  8847  hashf1lem1  13239  2swrdeqwrdeq  13453  rexfiuz  14087  modfsummods  14525  modfsummod  14526  coprmproddvdslem  15376  prmind2  15398  prmreclem2  15621  lubun  17123  efgsp1  18150  coe1fzgsumdlem  19671  evl1gsumdlem  19720  unocv  20024  basdif0  20757  isclo  20891  ordtrest2  21008  ptbasfi  21384  ptcnplem  21424  ptrescn  21442  ordthmeolem  21604  prdsxmetlem  22173  prdsbl  22296  iblcnlem1  23554  ellimc2  23641  rlimcnp  24692  xrlimcnp  24695  ftalem3  24801  dchreq  24983  2sqlem10  25153  dchrisum0flb  25199  pntpbnd1  25275  wlkp1lem8  26577  pthdlem1  26662  crctcshwlkn0lem7  26708  wwlksnext  26788  clwwlksel  26914  wwlksext2clwwlk  26924  3wlkdlem4  27022  3pthdlem1  27024  upgr4cycl4dv4e  27045  dfconngr1  27048  numclwwlkovf2exlem2  27212  ordtrest2NEW  29969  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem8  31180  ssltun1  31915  ssltun2  31916  hfext  32290  bj-raldifsn  33054  finixpnum  33394  lindsenlbs  33404  poimirlem26  33435  poimirlem27  33436  poimirlem32  33441  prdsbnd  33592  rrnequiv  33634  hdmap14lem13  37172  pfxsuffeqwrdeq  41406