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	$$⊢X=\bigcup A$$
	refbas.2	$$⊢Y=\bigcup B$$
Assertion	refbas	$$⊢A\mathrm{Ref}B\to Y=X$$

Proof

Step	Hyp	Ref	Expression
1		refbas.1	$$⊢X=\bigcup A$$
2		refbas.2	$$⊢Y=\bigcup B$$
3		refrel	$$⊢\mathrm{Rel}\mathrm{Ref}$$
4	3	brrelex1i	$$⊢A\mathrm{Ref}B\to A\in \mathrm{V}$$
5	1 2	isref	$$⊢A\in \mathrm{V}\to \left(A\mathrm{Ref}B\leftrightarrow \left(Y=X\wedge \forall x\in A\exists y\in Bx\subseteq y\right)\right)$$
6	5	simprbda	$$⊢\left(A\in \mathrm{V}\wedge A\mathrm{Ref}B\right)\to Y=X$$
7	4 6	mpancom	$$⊢A\mathrm{Ref}B\to Y=X$$