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

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.
StepHypRef Expression
1 df-iun 4332 . . 3
21releqi 5091 . 2
3 df-rel 5011 . 2
4 abss 3568 . . 3
5 df-rel 5011 . . . . . 6
6 dfss2 3492 . . . . . 6
75, 6bitri 249 . . . . 5
87ralbii 2888 . . . 4
9 ralcom4 3128 . . . 4
10 r19.23v 2937 . . . . 5
1110albii 1640 . . . 4
128, 9, 113bitri 271 . . 3
134, 12bitr4i 252 . 2
142, 3, 133bitri 271 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator