Metamath Proof Explorer


Theorem elxp5

Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 when the double intersection does not create class existence problems (caused by int0 ). (Contributed by NM, 1-Aug-2004)

Ref Expression
Assertion elxp5 A B × C A = A ran A A B ran A C

Proof

Step Hyp Ref Expression
1 elxp A B × C x y A = x y x B y C
2 sneq A = x y A = x y
3 2 rneqd A = x y ran A = ran x y
4 3 unieqd A = x y ran A = ran x y
5 vex x V
6 vex y V
7 5 6 op2nda ran x y = y
8 4 7 syl6req A = x y y = ran A
9 8 pm4.71ri A = x y y = ran A A = x y
10 9 anbi1i A = x y x B y C y = ran A A = x y x B y C
11 anass y = ran A A = x y x B y C y = ran A A = x y x B y C
12 10 11 bitri A = x y x B y C y = ran A A = x y x B y C
13 12 exbii y A = x y x B y C y y = ran A A = x y x B y C
14 snex A V
15 14 rnex ran A V
16 15 uniex ran A V
17 opeq2 y = ran A x y = x ran A
18 17 eqeq2d y = ran A A = x y A = x ran A
19 eleq1 y = ran A y C ran A C
20 19 anbi2d y = ran A x B y C x B ran A C
21 18 20 anbi12d y = ran A A = x y x B y C A = x ran A x B ran A C
22 16 21 ceqsexv y y = ran A A = x y x B y C A = x ran A x B ran A C
23 13 22 bitri y A = x y x B y C A = x ran A x B ran A C
24 inteq A = x ran A A = x ran A
25 24 inteqd A = x ran A A = x ran A
26 5 16 op1stb x ran A = x
27 25 26 syl6req A = x ran A x = A
28 27 pm4.71ri A = x ran A x = A A = x ran A
29 28 anbi1i A = x ran A x B ran A C x = A A = x ran A x B ran A C
30 anass x = A A = x ran A x B ran A C x = A A = x ran A x B ran A C
31 23 29 30 3bitri y A = x y x B y C x = A A = x ran A x B ran A C
32 31 exbii x y A = x y x B y C x x = A A = x ran A x B ran A C
33 eqvisset x = A A V
34 33 adantr x = A A = x ran A x B ran A C A V
35 34 exlimiv x x = A A = x ran A x B ran A C A V
36 elex A B A V
37 36 ad2antrl A = A ran A A B ran A C A V
38 opeq1 x = A x ran A = A ran A
39 38 eqeq2d x = A A = x ran A A = A ran A
40 eleq1 x = A x B A B
41 40 anbi1d x = A x B ran A C A B ran A C
42 39 41 anbi12d x = A A = x ran A x B ran A C A = A ran A A B ran A C
43 42 ceqsexgv A V x x = A A = x ran A x B ran A C A = A ran A A B ran A C
44 35 37 43 pm5.21nii x x = A A = x ran A x B ran A C A = A ran A A B ran A C
45 1 32 44 3bitri A B × C A = A ran A A B ran A C