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∈AB∩C=⨉x∈AB∩⨉x∈AC

Proof

Step Hyp Ref Expression
1 anandi ⊢fFnA∧∀x∈Af⁡x∈B∧∀x∈Af⁡x∈C↔fFnA∧∀x∈Af⁡x∈B∧fFnA∧∀x∈Af⁡x∈C
2 elin ⊢f⁡x∈B∩C↔f⁡x∈B∧f⁡x∈C
3 2 ralbii ⊢∀x∈Af⁡x∈B∩C↔∀x∈Af⁡x∈B∧f⁡x∈C
4 r19.26 ⊢∀x∈Af⁡x∈B∧f⁡x∈C↔∀x∈Af⁡x∈B∧∀x∈Af⁡x∈C
5 3 4 bitri ⊢∀x∈Af⁡x∈B∩C↔∀x∈Af⁡x∈B∧∀x∈Af⁡x∈C
6 5 anbi2i ⊢fFnA∧∀x∈Af⁡x∈B∩C↔fFnA∧∀x∈Af⁡x∈B∧∀x∈Af⁡x∈C
7 vex ⊢f∈V
8 7 elixp ⊢f∈⨉x∈AB↔fFnA∧∀x∈Af⁡x∈B
9 7 elixp ⊢f∈⨉x∈AC↔fFnA∧∀x∈Af⁡x∈C
10 8 9 anbi12i ⊢f∈⨉x∈AB∧f∈⨉x∈AC↔fFnA∧∀x∈Af⁡x∈B∧fFnA∧∀x∈Af⁡x∈C
11 1 6 10 3bitr4i ⊢fFnA∧∀x∈Af⁡x∈B∩C↔f∈⨉x∈AB∧f∈⨉x∈AC
12 7 elixp ⊢f∈⨉x∈AB∩C↔fFnA∧∀x∈Af⁡x∈B∩C
13 elin ⊢f∈⨉x∈AB∩⨉x∈AC↔f∈⨉x∈AB∧f∈⨉x∈AC
14 11 12 13 3bitr4i ⊢f∈⨉x∈AB∩C↔f∈⨉x∈AB∩⨉x∈AC
15 14 eqriv ⊢⨉x∈AB∩C=⨉x∈AB∩⨉x∈AC