Metamath Proof Explorer

Theorem ixpin

Description: The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Assertion ixpin ⊢ ⨉ x ∈ A B ∩ C = ⨉ x ∈ A B ∩ ⨉ x ∈ A C

Proof

Step Hyp Ref Expression
1 anandi ⊢ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B ∧ ∀ x ∈ A f ⁡ x ∈ C ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B ∧ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ C
2 elin ⊢ f ⁡ x ∈ B ∩ C ↔ f ⁡ x ∈ B ∧ f ⁡ x ∈ C
3 2 ralbii ⊢ ∀ x ∈ A f ⁡ x ∈ B ∩ C ↔ ∀ x ∈ A f ⁡ x ∈ B ∧ f ⁡ x ∈ C
4 r19.26 ⊢ ∀ x ∈ A f ⁡ x ∈ B ∧ f ⁡ x ∈ C ↔ ∀ x ∈ A f ⁡ x ∈ B ∧ ∀ x ∈ A f ⁡ x ∈ C
5 3 4 bitri ⊢ ∀ x ∈ A f ⁡ x ∈ B ∩ C ↔ ∀ x ∈ A f ⁡ x ∈ B ∧ ∀ x ∈ A f ⁡ x ∈ C
6 5 anbi2i ⊢ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B ∩ C ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B ∧ ∀ x ∈ A f ⁡ x ∈ C
7 vex ⊢ f ∈ V
8 7 elixp ⊢ f ∈ ⨉ x ∈ A B ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
9 7 elixp ⊢ f ∈ ⨉ x ∈ A C ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ C
10 8 9 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
11 1 6 10 3bitr4i ⊢ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B ∩ C ↔ f ∈ ⨉ x ∈ A B ∧ f ∈ ⨉ x ∈ A C
12 7 elixp ⊢ f ∈ ⨉ x ∈ A B ∩ C ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B ∩ C
13 elin ⊢ f ∈ ⨉ x ∈ A B ∩ ⨉ x ∈ A C ↔ f ∈ ⨉ x ∈ A B ∧ f ∈ ⨉ x ∈ A C
14 11 12 13 3bitr4i ⊢ f ∈ ⨉ x ∈ A B ∩ C ↔ f ∈ ⨉ x ∈ A B ∩ ⨉ x ∈ A C
15 14 eqriv ⊢ ⨉ x ∈ A B ∩ C = ⨉ x ∈ A B ∩ ⨉ x ∈ A C