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 𝑥𝐴 𝐵X 𝑥𝐴 𝐶 ) = X 𝑥𝐴 ( 𝐵𝐶 )

Proof

Step Hyp Ref Expression
1 an4 ( ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) ) ↔ ( ( 𝑓 Fn 𝐴𝑓 Fn 𝐴 ) ∧ ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) ) )
2 anidm ( ( 𝑓 Fn 𝐴𝑓 Fn 𝐴 ) ↔ 𝑓 Fn 𝐴 )
3 r19.26 ( ∀ 𝑥𝐴 ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑓𝑥 ) ∈ 𝐶 ) ↔ ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) )
4 elin ( ( 𝑓𝑥 ) ∈ ( 𝐵𝐶 ) ↔ ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑓𝑥 ) ∈ 𝐶 ) )
5 4 bicomi ( ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑓𝑥 ) ∈ 𝐶 ) ↔ ( 𝑓𝑥 ) ∈ ( 𝐵𝐶 ) )
6 5 ralbii ( ∀ 𝑥𝐴 ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑓𝑥 ) ∈ 𝐶 ) ↔ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ ( 𝐵𝐶 ) )
7 3 6 bitr3i ( ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) ↔ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ ( 𝐵𝐶 ) )
8 2 7 anbi12i ( ( ( 𝑓 Fn 𝐴𝑓 Fn 𝐴 ) ∧ ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ ( 𝐵𝐶 ) ) )
9 1 8 bitri ( ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ ( 𝐵𝐶 ) ) )
10 vex 𝑓 ∈ V
11 10 elixp ( 𝑓X 𝑥𝐴 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
12 10 elixp ( 𝑓X 𝑥𝐴 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) )
13 11 12 anbi12i ( ( 𝑓X 𝑥𝐴 𝐵𝑓X 𝑥𝐴 𝐶 ) ↔ ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐶 ) ) )
14 10 elixp ( 𝑓X 𝑥𝐴 ( 𝐵𝐶 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ ( 𝐵𝐶 ) ) )
15 9 13 14 3bitr4i ( ( 𝑓X 𝑥𝐴 𝐵𝑓X 𝑥𝐴 𝐶 ) ↔ 𝑓X 𝑥𝐴 ( 𝐵𝐶 ) )
16 15 ineqri ( X 𝑥𝐴 𝐵X 𝑥𝐴 𝐶 ) = X 𝑥𝐴 ( 𝐵𝐶 )