Metamath Proof Explorer


Theorem relun

Description: The union of two relations is a relation. Compare Exercise 5 of TakeutiZaring p. 25. (Contributed by NM, 12-Aug-1994)

Ref Expression
Assertion relun ( Rel ( 𝐴𝐵 ) ↔ ( Rel 𝐴 ∧ Rel 𝐵 ) )

Proof

Step Hyp Ref Expression
1 unss ( ( 𝐴 ⊆ ( V × V ) ∧ 𝐵 ⊆ ( V × V ) ) ↔ ( 𝐴𝐵 ) ⊆ ( V × V ) )
2 df-rel ( Rel 𝐴𝐴 ⊆ ( V × V ) )
3 df-rel ( Rel 𝐵𝐵 ⊆ ( V × V ) )
4 2 3 anbi12i ( ( Rel 𝐴 ∧ Rel 𝐵 ) ↔ ( 𝐴 ⊆ ( V × V ) ∧ 𝐵 ⊆ ( V × V ) ) )
5 df-rel ( Rel ( 𝐴𝐵 ) ↔ ( 𝐴𝐵 ) ⊆ ( V × V ) )
6 1 4 5 3bitr4ri ( Rel ( 𝐴𝐵 ) ↔ ( Rel 𝐴 ∧ Rel 𝐵 ) )