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

Proof

Step Hyp Ref Expression
1 refbas.1 
 |-  X = U. A
2 refbas.2 
 |-  Y = U. B
3 refrel 
 |-  Rel Ref
4 3 brrelex1i 
 |-  ( A Ref B -> A e. _V )
5 1 2 isref 
 |-  ( A e. _V -> ( A Ref B <-> ( Y = X /\ A. x e. A E. y e. B x C_ y ) ) )
6 5 simprbda 
 |-  ( ( A e. _V /\ A Ref B ) -> Y = X )
7 4 6 mpancom 
 |-  ( A Ref B -> Y = X )