Theorem reliun 5772

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 4987	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ (V × V) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ (V × V))
2		df-rel 5638	. 2 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ (V × V))
3		df-rel 5638	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
4	3	ralbii 3083	. 2 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ (V × V))
5	1, 2, 4	3bitr4i 303	1 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵)

Syntax hints:   ↔ wb 206  ∀wral 3051  Vcvv 3429   ⊆ wss 3889  ∪ ciun 4933   × cxp 5629  Rel wrel 5636

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-v 3431  df-ss 3906  df-iun 4935  df-rel 5638

This theorem is referenced by:  reluni  5774  eliunxp  5792  opeliunxp2  5793  dfco2  6209  coiun  6221  fvn0ssdmfun  7026  opeliunxp2f  8160  fsumcom2  15736  fprodcom2  15949  imasaddfnlem  17492  imasvscafn  17501  gsum2d2lem  19948  gsum2d2  19949  gsumcom2  19950  dprd2d2  20021  cnextrel  24028  reldv  25837  dfcnv2  32748  gsumpart  33124  gsumwrd2dccat  33139  cvmliftlem1  35467  cnviun  44077  coiun1  44079  eliunxp2  48810