Theorem reliun 5123

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 4327	. . 3 |- U_ x e. A B = { y | E. x e. A y e. B }
2	1	releqi 5086	. 2 |- ( Rel U_ x e. A B <-> Rel { y | E. x e. A y e. B } )
3		df-rel 5006	. 2 |- ( Rel { y | E. x e. A y e. B } <-> { y | E. x e. A y e. B } C_ ( _V X. _V ) )
4		abss 3569	. . 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 5006	. . . . . 6 |- ( Rel B <-> B C_ ( _V X. _V ) )
6		dfss2 3493	. . . . . 6 |- ( B C_ ( _V X. _V ) <-> A. y ( y e. B -> y e. ( _V X. _V ) ) )
7	5, 6	bitri 249	. . . . 5 |- ( Rel B <-> A. y ( y e. B -> y e. ( _V X. _V ) ) )
8	7	ralbii 2895	. . . 4 |- ( A. x e. A Rel B <-> A. x e. A A. y ( y e. B -> y e. ( _V X. _V ) ) )
9		ralcom4 3132	. . . 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 2943	. . . . 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 1620	. . . 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 271	. . 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 252	. 2 |- ( { y | E. x e. A y e. B } C_ ( _V X. _V ) <-> A. x e. A Rel B )
14	2, 3, 13	3bitri 271	1 |- ( Rel U_ x e. A B <-> A. x e. A Rel B )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1377   e. wcel 1767   {cab 2452   A.wral 2814   E.wrex 2815   _Vcvv 3113   C_ wss 3476   U_ciun 4325   X. cxp 4997   Rel wrel 5004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-iun 4327  df-rel 5006

This theorem is referenced by:  reluni  5125  eliunxp  5140  opeliunxp2  5141  dfco2  5506  coiun  5517  fsumcom2  13555  imasaddfnlem  14786  imasvscafn  14795  gsum2d2lem  16816  gsum2d2  16817  gsumcom2  16818  dprd2d2  16907  cnextrel  20390  reldv  22101  dfcnv2  27286  cvmliftlem1  28481  fprodcom2  28967  eliunxp2  32218