# 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 ${⊢}\underset{{x}\in {A}}{⨉}{B}\cap \underset{{x}\in {A}}{⨉}{C}=\underset{{x}\in {A}}{⨉}\left({B}\cap {C}\right)$

### Proof

Step Hyp Ref Expression
1 an4 ${⊢}\left(\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\wedge \left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\right)↔\left(\left({f}Fn{A}\wedge {f}Fn{A}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\right)$
2 anidm ${⊢}\left({f}Fn{A}\wedge {f}Fn{A}\right)↔{f}Fn{A}$
3 r19.26 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in {B}\wedge {f}\left({x}\right)\in {C}\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)$
4 elin ${⊢}{f}\left({x}\right)\in \left({B}\cap {C}\right)↔\left({f}\left({x}\right)\in {B}\wedge {f}\left({x}\right)\in {C}\right)$
5 4 bicomi ${⊢}\left({f}\left({x}\right)\in {B}\wedge {f}\left({x}\right)\in {C}\right)↔{f}\left({x}\right)\in \left({B}\cap {C}\right)$
6 5 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in {B}\wedge {f}\left({x}\right)\in {C}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({B}\cap {C}\right)$
7 3 6 bitr3i ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({B}\cap {C}\right)$
8 2 7 anbi12i ${⊢}\left(\left({f}Fn{A}\wedge {f}Fn{A}\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\right)↔\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({B}\cap {C}\right)\right)$
9 1 8 bitri ${⊢}\left(\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\wedge \left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\right)↔\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({B}\cap {C}\right)\right)$
10 vex ${⊢}{f}\in \mathrm{V}$
11 10 elixp ${⊢}{f}\in \underset{{x}\in {A}}{⨉}{B}↔\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$
12 10 elixp ${⊢}{f}\in \underset{{x}\in {A}}{⨉}{C}↔\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)$
13 11 12 anbi12i ${⊢}\left({f}\in \underset{{x}\in {A}}{⨉}{B}\wedge {f}\in \underset{{x}\in {A}}{⨉}{C}\right)↔\left(\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\wedge \left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {C}\right)\right)$
14 10 elixp ${⊢}{f}\in \underset{{x}\in {A}}{⨉}\left({B}\cap {C}\right)↔\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({B}\cap {C}\right)\right)$
15 9 13 14 3bitr4i ${⊢}\left({f}\in \underset{{x}\in {A}}{⨉}{B}\wedge {f}\in \underset{{x}\in {A}}{⨉}{C}\right)↔{f}\in \underset{{x}\in {A}}{⨉}\left({B}\cap {C}\right)$
16 15 ineqri ${⊢}\underset{{x}\in {A}}{⨉}{B}\cap \underset{{x}\in {A}}{⨉}{C}=\underset{{x}\in {A}}{⨉}\left({B}\cap {C}\right)$