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	⊢ ( ( 𝐵 ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ∈ V ) → 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		dmexg	⊢ ( ( 𝐴 × 𝐵 ) ∈ V → dom ( 𝐴 × 𝐵 ) ∈ V )
2		dmxp	⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
3	2	eleq1d	⊢ ( 𝐵 ≠ ∅ → ( dom ( 𝐴 × 𝐵 ) ∈ V ↔ 𝐴 ∈ V ) )
4	1 3	imbitrid	⊢ ( 𝐵 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ V → 𝐴 ∈ V ) )
5	4	imp	⊢ ( ( 𝐵 ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ∈ V ) → 𝐴 ∈ V )