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	⊢ 𝑋 = ∪ 𝐴
	fnebas.2	⊢ 𝑌 = ∪ 𝐵
Assertion	fnebas	⊢ ( 𝐴 Fne 𝐵 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		fnebas.1	⊢ 𝑋 = ∪ 𝐴
2		fnebas.2	⊢ 𝑌 = ∪ 𝐵
3	1 2	isfne4	⊢ ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
4	3	simplbi	⊢ ( 𝐴 Fne 𝐵 → 𝑋 = 𝑌 )