Metamath Proof Explorer


Theorem inixp

Description: Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion inixp x A B x A C = x A B C

Proof

Step Hyp Ref Expression
1 an4 f Fn A x A f x B f Fn A x A f x C f Fn A f Fn A x A f x B x A f x C
2 anidm f Fn A f Fn A f Fn A
3 r19.26 x A f x B f x C x A f x B x A f x C
4 elin f x B C f x B f x C
5 4 bicomi f x B f x C f x B C
6 5 ralbii x A f x B f x C x A f x B C
7 3 6 bitr3i x A f x B x A f x C x A f x B C
8 2 7 anbi12i f Fn A f Fn A x A f x B x A f x C f Fn A x A f x B C
9 1 8 bitri f Fn A x A f x B f Fn A x A f x C f Fn A x A f x B C
10 vex f V
11 10 elixp f x A B f Fn A x A f x B
12 10 elixp f x A C f Fn A x A f x C
13 11 12 anbi12i f x A B f x A C f Fn A x A f x B f Fn A x A f x C
14 10 elixp f x A B C f Fn A x A f x B C
15 9 13 14 3bitr4i f x A B f x A C f x A B C
16 15 ineqri x A B x A C = x A B C