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