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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elxp | |
|
2 | df-rex | |
|
3 | an13 | |
|
4 | 3 | exbii | |
5 | 2 4 | bitr4i | |
6 | elsni | |
|
7 | 6 | opeq1d | |
8 | 7 | eqeq2d | |
9 | 8 | biimpa | |
10 | 9 | reximi | |
11 | 5 10 | sylbir | |
12 | 11 | exlimiv | |
13 | 1 12 | sylbi | |
14 | snidg | |
|
15 | opelxpi | |
|
16 | 14 15 | sylan | |
17 | eleq1 | |
|
18 | 16 17 | syl5ibrcom | |
19 | 18 | rexlimdva | |
20 | 13 19 | impbid2 | |