Metamath Proof Explorer

Theorem bj-xpima1snALT

Description: Alternate proof of bj-xpima1sn . (Contributed by BJ, 6-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 disjsn 
 |-  ( ( A i^i { X } ) = (/) <-> -. X e. A )
2 xpima1 
 |-  ( ( A i^i { X } ) = (/) -> ( ( A X. B ) " { X } ) = (/) )
3 1 2 sylbir 
 |-  ( -. X e. A -> ( ( A X. B ) " { X } ) = (/) )