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

Proof

Step Hyp Ref Expression
1 an4 ⊢fFnA∧∀x∈Af⁡x∈B∧fFnA∧∀x∈Af⁡x∈C↔fFnA∧fFnA∧∀x∈Af⁡x∈B∧∀x∈Af⁡x∈C
2 anidm ⊢fFnA∧fFnA↔fFnA
3 r19.26 ⊢∀x∈Af⁡x∈B∧f⁡x∈C↔∀x∈Af⁡x∈B∧∀x∈Af⁡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∈Af⁡x∈B∧f⁡x∈C↔∀x∈Af⁡x∈B∩C
7 3 6 bitr3i ⊢∀x∈Af⁡x∈B∧∀x∈Af⁡x∈C↔∀x∈Af⁡x∈B∩C
8 2 7 anbi12i ⊢fFnA∧fFnA∧∀x∈Af⁡x∈B∧∀x∈Af⁡x∈C↔fFnA∧∀x∈Af⁡x∈B∩C
9 1 8 bitri ⊢fFnA∧∀x∈Af⁡x∈B∧fFnA∧∀x∈Af⁡x∈C↔fFnA∧∀x∈Af⁡x∈B∩C
10 vex ⊢f∈V
11 10 elixp ⊢f∈⨉x∈AB↔fFnA∧∀x∈Af⁡x∈B
12 10 elixp ⊢f∈⨉x∈AC↔fFnA∧∀x∈Af⁡x∈C
13 11 12 anbi12i ⊢f∈⨉x∈AB∧f∈⨉x∈AC↔fFnA∧∀x∈Af⁡x∈B∧fFnA∧∀x∈Af⁡x∈C
14 10 elixp ⊢f∈⨉x∈AB∩C↔fFnA∧∀x∈Af⁡x∈B∩C
15 9 13 14 3bitr4i ⊢f∈⨉x∈AB∧f∈⨉x∈AC↔f∈⨉x∈AB∩C
16 15 ineqri ⊢⨉x∈AB∩⨉x∈AC=⨉x∈AB∩C