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 >. ) )