Theorem fnebas

Description: A finer cover covers the same set as the original. (Contributed by Jeff Hankins, 28-Sep-2009)

	Ref	Expression
Hypotheses	fnebas.1	$$⊢X=\bigcup A$$
	fnebas.2	$$⊢Y=\bigcup B$$
Assertion	fnebas	$$⊢A\mathrm{Fne}B\to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		fnebas.1	$$⊢X=\bigcup A$$
2		fnebas.2	$$⊢Y=\bigcup B$$
3	1 2	isfne4	$$⊢A\mathrm{Fne}B\leftrightarrow \left(X=Y\wedge A\subseteq \mathrm{topGen}\left(B\right)\right)$$
4	3	simplbi	$$⊢A\mathrm{Fne}B\to X=Y$$