Metamath Proof Explorer

Theorem xpimasn

Description: Direct image of a singleton by a Cartesian product. (Contributed by Thierry Arnoux, 14-Jan-2018) (Proof shortened by BJ, 6-Apr-2019)

Ref Expression
Assertion xpimasn 
|- ( X e. A -> ( ( A X. B ) " { X } ) = B )

Proof

Step Hyp Ref Expression
1 disjsn 
 |-  ( ( A i^i { X } ) = (/) <-> -. X e. A )
2 1 necon3abii 
 |-  ( ( A i^i { X } ) =/= (/) <-> -. -. X e. A )
3 notnotb 
 |-  ( X e. A <-> -. -. X e. A )
4 2 3 bitr4i 
 |-  ( ( A i^i { X } ) =/= (/) <-> X e. A )
5 xpima2 
 |-  ( ( A i^i { X } ) =/= (/) -> ( ( A X. B ) " { X } ) = B )
6 4 5 sylbir 
 |-  ( X e. A -> ( ( A X. B ) " { X } ) = B )