Metamath Proof Explorer

Theorem xpexcnv

Description: A condition where the converse of xpex holds as well. Corollary 6.9(2) in TakeutiZaring p. 26. (Contributed by Andrew Salmon, 13-Nov-2011)

Ref Expression
Assertion xpexcnv B A × B V A V


Step Hyp Ref Expression
1 dmexg A × B V dom A × B V
2 dmxp B dom A × B = A
3 2 eleq1d B dom A × B V A V
4 1 3 syl5ib B A × B V A V
5 4 imp B A × B V A V