Theorem reliun 5805

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wral 3081  Vcvv 3457   ⊆ wss 3906  ∪ ciun 4958   × cxp 5661  Rel wrel 5668

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 2148  ax-9 2156  ax-11 2195  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-ss 3923  df-iun 4960  df-rel 5670

This theorem is used by:  reluni  5807  eliunxp  5825  opeliunxp2  5826  dfco2  6248  coiun  6260  fvn0ssdmfun  7073  opeliunxp2f  8212  fsumcom2  15852  fprodcom2  16065  imasaddfnlem  17608  imasvscafn  17617  gsum2d2lem  20091  gsum2d2  20092  gsumcom2  20093  dprd2d2  20164  cnextrel  24275  reldv  26084  dfcnv2  33095  gsumpart  33451  gsumwrd2dccat  33466  cvmliftlem1  35818  cnviun  44453  coiun1  44455  eliunxp2  49190