Metamath Proof Explorer


Theorem elxp8

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 . (Contributed by ML, 19-Oct-2020)

Ref Expression
Assertion elxp8 A B × C 1 st A B A V × C

Proof

Step Hyp Ref Expression
1 xp1st A B × C 1 st A B
2 ssv B V
3 ssid C C
4 xpss12 B V C C B × C V × C
5 2 3 4 mp2an B × C V × C
6 5 sseli A B × C A V × C
7 1 6 jca A B × C 1 st A B A V × C
8 xpss V × C V × V
9 8 sseli A V × C A V × V
10 9 adantl 1 st A B A V × C A V × V
11 xp2nd A V × C 2 nd A C
12 11 anim2i 1 st A B A V × C 1 st A B 2 nd A C
13 elxp7 A B × C A V × V 1 st A B 2 nd A C
14 10 12 13 sylanbrc 1 st A B A V × C A B × C
15 7 14 impbii A B × C 1 st A B A V × C