Description: Intersection of two Cartesian products. Exercise 9 of TakeutiZaring p. 25. (Contributed by NM, 3-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | inxp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inopab | |
|
2 | an4 | |
|
3 | elin | |
|
4 | elin | |
|
5 | 3 4 | anbi12i | |
6 | 2 5 | bitr4i | |
7 | 6 | opabbii | |
8 | 1 7 | eqtri | |
9 | df-xp | |
|
10 | df-xp | |
|
11 | 9 10 | ineq12i | |
12 | df-xp | |
|
13 | 8 11 12 | 3eqtr4i | |