Theorem reliun 5775

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

Assertion

Ref	Expression
reliun	⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵)

Proof of Theorem reliun

Step	Hyp	Ref	Expression
1		iunss 5002	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ (V × V) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ (V × V))
2		df-rel 5641	. 2 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ (V × V))
3		df-rel 5641	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
4	3	ralbii 3084	. 2 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ (V × V))
5	1, 2, 4	3bitr4i 303	1 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵)

Syntax hints:   ↔ wb 206  ∀wral 3052  Vcvv 3442   ⊆ wss 3903  ∪ ciun 4948   × cxp 5632  Rel wrel 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3444  df-ss 3920  df-iun 4950  df-rel 5641

This theorem is referenced by:  reluni  5777  eliunxp  5796  opeliunxp2  5797  dfco2  6213  coiun  6225  fvn0ssdmfun  7030  opeliunxp2f  8164  fsumcom2  15711  fprodcom2  15921  imasaddfnlem  17463  imasvscafn  17472  gsum2d2lem  19919  gsum2d2  19920  gsumcom2  19921  dprd2d2  19992  cnextrel  24024  reldv  25844  dfcnv2  32771  gsumpart  33163  gsumwrd2dccat  33178  cvmliftlem1  35507  cnviun  44035  coiun1  44037  eliunxp2  48723