Theorem reliun 5128

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

Proof of Theorem reliun

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4332	. . 3
2	1	releqi 5091	. 2
3		df-rel 5011	. 2
4		abss 3568	. . 3
5		df-rel 5011	. . . . . 6
6		dfss2 3492	. . . . . 6
7	5, 6	bitri 249	. . . . 5
8	7	ralbii 2888	. . . 4
9		ralcom4 3128	. . . 4
10		r19.23v 2937	. . . . 5
11	10	albii 1640	. . . 4
12	8, 9, 11	3bitri 271	. . 3
13	4, 12	bitr4i 252	. 2
14	2, 3, 13	3bitri 271	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  e.wcel 1818  {cab 2442  A.wral 2807  E.wrex 2808  cvv 3109  C_wss 3475  U_ciun 4330  X.cxp 5002  Relwrel 5009

This theorem is referenced by:  reluni  5130  eliunxp  5145  opeliunxp2  5146  dfco2  5511  coiun  5522  fvn0ssdmfun  6022  fsumcom2  13589  fprodcom2  13788  imasaddfnlem  14925  imasvscafn  14934  gsum2d2lem  17001  gsum2d2  17002  gsumcom2  17003  dprd2d2  17093  cnextrel  20563  reldv  22274  dfcnv2  27517  cvmliftlem1  28730  eliunxp2  32923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-iun 4332  df-rel 5011