Theorem refbas

Description: A refinement covers the same set. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

	Ref	Expression
Hypotheses	refbas.1	⊢ 𝑋 = ∪ 𝐴
	refbas.2	⊢ 𝑌 = ∪ 𝐵
Assertion	refbas	⊢ ( 𝐴 Ref 𝐵 → 𝑌 = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		refbas.1	⊢ 𝑋 = ∪ 𝐴
2		refbas.2	⊢ 𝑌 = ∪ 𝐵
3		refrel	⊢ Rel Ref
4	3	brrelex1i	⊢ ( 𝐴 Ref 𝐵 → 𝐴 ∈ V )
5	1 2	isref	⊢ ( 𝐴 ∈ V → ( 𝐴 Ref 𝐵 ↔ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
6	5	simprbda	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 Ref 𝐵 ) → 𝑌 = 𝑋 )
7	4 6	mpancom	⊢ ( 𝐴 Ref 𝐵 → 𝑌 = 𝑋 )