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	$$⊢\left(B\ne \varnothing \wedge A\times B\in \mathrm{V}\right)\to A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dmexg	$$⊢A\times B\in \mathrm{V}\to \mathrm{dom}\left(A\times B\right)\in \mathrm{V}$$
2		dmxp	$$⊢B\ne \varnothing \to \mathrm{dom}\left(A\times B\right)=A$$
3	2	eleq1d	$$⊢B\ne \varnothing \to \left(\mathrm{dom}\left(A\times B\right)\in \mathrm{V}\leftrightarrow A\in \mathrm{V}\right)$$
4	1 3	syl5ib	$$⊢B\ne \varnothing \to \left(A\times B\in \mathrm{V}\to A\in \mathrm{V}\right)$$
5	4	imp	$$⊢\left(B\ne \varnothing \wedge A\times B\in \mathrm{V}\right)\to A\in \mathrm{V}$$