This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elsnxp

Description: Membership in a Cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion elsnxp 
|- ( X e. V -> ( Z e. ( { X } X. A ) <-> E. y e. A Z = <. X , y >. ) )

Proof

Step Hyp Ref Expression
1 elxp 
 |-  ( Z e. ( { X } X. A ) <-> E. x E. y ( Z = <. x , y >. /\ ( x e. { X } /\ y e. A ) ) )
2 df-rex 
 |-  ( E. y e. A ( x e. { X } /\ Z = <. x , y >. ) <-> E. y ( y e. A /\ ( x e. { X } /\ Z = <. x , y >. ) ) )
3 an13 
 |-  ( ( Z = <. x , y >. /\ ( x e. { X } /\ y e. A ) ) <-> ( y e. A /\ ( x e. { X } /\ Z = <. x , y >. ) ) )
4 3 exbii 
 |-  ( E. y ( Z = <. x , y >. /\ ( x e. { X } /\ y e. A ) ) <-> E. y ( y e. A /\ ( x e. { X } /\ Z = <. x , y >. ) ) )
5 2 4 bitr4i 
 |-  ( E. y e. A ( x e. { X } /\ Z = <. x , y >. ) <-> E. y ( Z = <. x , y >. /\ ( x e. { X } /\ y e. A ) ) )
6 elsni 
 |-  ( x e. { X } -> x = X )
7 6 opeq1d 
 |-  ( x e. { X } -> <. x , y >. = <. X , y >. )
8 7 eqeq2d 
 |-  ( x e. { X } -> ( Z = <. x , y >. <-> Z = <. X , y >. ) )
9 8 biimpa 
 |-  ( ( x e. { X } /\ Z = <. x , y >. ) -> Z = <. X , y >. )
10 9 reximi 
 |-  ( E. y e. A ( x e. { X } /\ Z = <. x , y >. ) -> E. y e. A Z = <. X , y >. )
11 5 10 sylbir 
 |-  ( E. y ( Z = <. x , y >. /\ ( x e. { X } /\ y e. A ) ) -> E. y e. A Z = <. X , y >. )
12 11 exlimiv 
 |-  ( E. x E. y ( Z = <. x , y >. /\ ( x e. { X } /\ y e. A ) ) -> E. y e. A Z = <. X , y >. )
13 1 12 sylbi 
 |-  ( Z e. ( { X } X. A ) -> E. y e. A Z = <. X , y >. )
14 snidg 
 |-  ( X e. V -> X e. { X } )
15 opelxpi 
 |-  ( ( X e. { X } /\ y e. A ) -> <. X , y >. e. ( { X } X. A ) )
16 14 15 sylan 
 |-  ( ( X e. V /\ y e. A ) -> <. X , y >. e. ( { X } X. A ) )
17 eleq1 
 |-  ( Z = <. X , y >. -> ( Z e. ( { X } X. A ) <-> <. X , y >. e. ( { X } X. A ) ) )
18 16 17 syl5ibrcom 
 |-  ( ( X e. V /\ y e. A ) -> ( Z = <. X , y >. -> Z e. ( { X } X. A ) ) )
19 18 rexlimdva 
 |-  ( X e. V -> ( E. y e. A Z = <. X , y >. -> Z e. ( { X } X. A ) ) )
20 13 19 impbid2 
 |-  ( X e. V -> ( Z e. ( { X } X. A ) <-> E. y e. A Z = <. X , y >. ) )