Theorem refrel

Description: Refinement is a relation. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

	Ref	Expression
Assertion	refrel	⊢ Rel Ref

Proof

Step	Hyp	Ref	Expression
1		df-ref	⊢ Ref = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∪ 𝑦 = ∪ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) }
2	1	relopabiv	⊢ Rel Ref