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 = U. A
	fnebas.2	|- Y = U. B
Assertion	fnebas	|- ( A Fne B -> X = Y )

Proof

Step	Hyp	Ref	Expression
1		fnebas.1	|- X = U. A
2		fnebas.2	|- Y = U. B
3	1 2	isfne4	|- ( A Fne B <-> ( X = Y /\ A C_ ( topGen ` B ) ) )
4	3	simplbi	|- ( A Fne B -> X = Y )