This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ⋃ A
fnebas.2 ⊢ Y = ⋃ B
Assertion fnebas ⊢ A Fne B → X = Y

Proof

Step Hyp Ref Expression
1 fnebas.1 ⊢ X = ⋃ A
2 fnebas.2 ⊢ Y = ⋃ B
3 1 2 isfne4 ⊢ A Fne B ↔ X = Y ∧ A ⊆ topGen ⁡ B
4 3 simplbi ⊢ A Fne B → X = Y