Theorem reliun 4974

Description: An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.)

Assertion

Ref	Expression
reliun	|- ( Rel U_ x e. A B <-> A. x e. A Rel B )

Proof of Theorem reliun

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4304	. . 3 |- U_ x e. A B = { y | E. x e. A y e. B }
2	1	releqi 4938	. 2 |- ( Rel U_ x e. A B <-> Rel { y | E. x e. A y e. B } )
3		df-rel 4861	. 2 |- ( Rel { y | E. x e. A y e. B } <-> { y | E. x e. A y e. B } C_ ( _V X. _V ) )
4		abss 3536	. . 3 |- ( { y | E. x e. A y e. B } C_ ( _V X. _V ) <-> A. y ( E. x e. A y e. B -> y e. ( _V X. _V ) ) )
5		df-rel 4861	. . . . . 6 |- ( Rel B <-> B C_ ( _V X. _V ) )
6		dfss2 3459	. . . . . 6 |- ( B C_ ( _V X. _V ) <-> A. y ( y e. B -> y e. ( _V X. _V ) ) )
7	5, 6	bitri 252	. . . . 5 |- ( Rel B <-> A. y ( y e. B -> y e. ( _V X. _V ) ) )
8	7	ralbii 2863	. . . 4 |- ( A. x e. A Rel B <-> A. x e. A A. y ( y e. B -> y e. ( _V X. _V ) ) )
9		ralcom4 3106	. . . 4 |- ( A. x e. A A. y ( y e. B -> y e. ( _V X. _V ) ) <-> A. y A. x e. A ( y e. B -> y e. ( _V X. _V ) ) )
10		r19.23v 2912	. . . . 5 |- ( A. x e. A ( y e. B -> y e. ( _V X. _V ) ) <-> ( E. x e. A y e. B -> y e. ( _V X. _V ) ) )
11	10	albii 1687	. . . 4 |- ( A. y A. x e. A ( y e. B -> y e. ( _V X. _V ) ) <-> A. y ( E. x e. A y e. B -> y e. ( _V X. _V ) ) )
12	8, 9, 11	3bitri 274	. . 3 |- ( A. x e. A Rel B <-> A. y ( E. x e. A y e. B -> y e. ( _V X. _V ) ) )
13	4, 12	bitr4i 255	. 2 |- ( { y | E. x e. A y e. B } C_ ( _V X. _V ) <-> A. x e. A Rel B )
14	2, 3, 13	3bitri 274	1 |- ( Rel U_ x e. A B <-> A. x e. A Rel B )

Syntax hints:   -> wi 4   <-> wb 187   A.wal 1435   e. wcel 1870   {cab 2414   A.wral 2782   E.wrex 2783   _Vcvv 3087   C_ wss 3442   U_ciun 4302   X. cxp 4852   Rel wrel 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-v 3089  df-in 3449  df-ss 3456  df-iun 4304  df-rel 4861

This theorem is referenced by:  reluni  4976  eliunxp  4992  opeliunxp2  4993  dfco2  5354  coiun  5365  fvn0ssdmfun  6028  fsumcom2  13813  fprodcom2  14016  imasaddfnlem  15385  imasvscafn  15394  gsum2d2lem  17540  gsum2d2  17541  gsumcom2  17542  dprd2d2  17612  cnextrel  21009  reldv  22702  dfcnv2  28119  cvmliftlem1  29796  cnviun  35884  coiun1  35886  eliunxp2  38887