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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 refbas.1 ⊢ X = ⋃ A
2 refbas.2 ⊢ Y = ⋃ B
3 refrel ⊢ Rel ⁡ Ref
4 3 brrelex1i ⊢ A Ref B → A ∈ V
5 1 2 isref ⊢ A ∈ V → A Ref B ↔ Y = X ∧ ∀ x ∈ A ∃ y ∈ B x ⊆ y
6 5 simprbda ⊢ A ∈ V ∧ A Ref B → Y = X
7 4 6 mpancom ⊢ A Ref B → Y = X