Theorem reliun 5794

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wral 3077  Vcvv 3451   ⊆ wss 3899  ∪ ciun 4951   × cxp 5649  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3453  df-ss 3916  df-iun 4953  df-rel 5658

This theorem is used by:  reluni  5796  eliunxp  5814  opeliunxp2  5815  dfco2  6246  coiun  6258  fvn0ssdmfun  7074  opeliunxp2f  8227  fsumcom2  15940  fprodcom2  16151  imasaddfnlem  17700  imasvscafn  17709  gsum2d2lem  20187  gsum2d2  20188  gsumcom2  20189  dprd2d2  20260  cnextrel  24382  reldv  26190  dfcnv2  33269  gsumpart  33624  gsumwrd2dccat  33639  cvmliftlem1  36050  cnviun  44649  coiun1  44651  eliunxp2  49445