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 XVZX×AyAZ=Xy

Proof

Step Hyp Ref Expression
1 elxp ZX×AxyZ=xyxXyA
2 df-rex yAxXZ=xyyyAxXZ=xy
3 an13 Z=xyxXyAyAxXZ=xy
4 3 exbii yZ=xyxXyAyyAxXZ=xy
5 2 4 bitr4i yAxXZ=xyyZ=xyxXyA
6 elsni xXx=X
7 6 opeq1d xXxy=Xy
8 7 eqeq2d xXZ=xyZ=Xy
9 8 biimpa xXZ=xyZ=Xy
10 9 reximi yAxXZ=xyyAZ=Xy
11 5 10 sylbir yZ=xyxXyAyAZ=Xy
12 11 exlimiv xyZ=xyxXyAyAZ=Xy
13 1 12 sylbi ZX×AyAZ=Xy
14 snidg XVXX
15 opelxpi XXyAXyX×A
16 14 15 sylan XVyAXyX×A
17 eleq1 Z=XyZX×AXyX×A
18 16 17 syl5ibrcom XVyAZ=XyZX×A
19 18 rexlimdva XVyAZ=XyZX×A
20 13 19 impbid2 XVZX×AyAZ=Xy