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

Theorem reliun 4987
 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 4087 . . 3
21releqi 4952 . 2
3 df-rel 4877 . 2
4 abss 3404 . . 3
5 df-rel 4877 . . . . . 6
6 dfss2 3329 . . . . . 6
75, 6bitri 241 . . . . 5
87ralbii 2721 . . . 4
9 ralcom4 2966 . . . 4
10 r19.23v 2814 . . . . 5
1110albii 1575 . . . 4
128, 9, 113bitri 263 . . 3
134, 12bitr4i 244 . 2
142, 3, 133bitri 263 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177  wal 1549   wcel 1725  cab 2421  wral 2697  wrex 2698  cvv 2948   wss 3312  ciun 4085   cxp 4868   wrel 4875 This theorem is referenced by:  reluni  4989  eliunxp  5004  opeliunxp2  5005  dfco2  5361  coiun  5371  fsumcom2  12550  imasaddfnlem  13745  imasvscafn  13754  gsum2d2lem  15539  gsum2d2  15540  gsumcom2  15541  dprd2d2  15594  cnextrel  18086  reldv  19749  cvmliftlem1  24964  fprodcom2  25300 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-v 2950  df-in 3319  df-ss 3326  df-iun 4087  df-rel 4877
 Copyright terms: Public domain W3C validator